Erdős Problem 1212

References:

• erdosproblems.com/1212
• [Er80] Erdős, P., Some notes on problems and results in number theory (1980), p. 114.

This file also records machine-checked cores of verified partial results (2026): a composite-anchor sufficient reduction and an impossibility theorem for periodic certificates; see the corresponding lemmas below.

def Erdos1212.Valid (p : ℕ × ℕ) : Prop

A vertex of the strengthened problem: a visible lattice point with both coordinates exceeding 1 and at least one coordinate composite.

Equations

• Erdos1212.Valid p = (1 < p.1 ∧ 1 < p.2 ∧ p.1.gcd p.2 = 1 ∧ (¬Nat.Prime p.1 ∨ ¬Nat.Prime p.2))

theorem Erdos1212.valid_four_three : Valid (4, 3)

Sanity check for Valid: the vertex $(4, 3)$ is valid — both coordinates exceed $1$, they are coprime, and $4$ is composite.

def Erdos1212.Adj (p q : ℕ × ℕ) : Prop

Two lattice points are adjacent iff they differ by exactly 1 in exactly one coordinate.

Equations

• Erdos1212.Adj p q = (p.1 = q.1 ∧ (p.2 = q.2 + 1 ∨ q.2 = p.2 + 1) ∨ p.2 = q.2 ∧ (p.1 = q.1 + 1 ∨ q.1 = p.1 + 1))

theorem Erdos1212.erdos_1212 : sorry ↔ ∃ (f : ℕ → ℕ × ℕ), Function.Injective f ∧ (∀ (n : ℕ), Adj (f n) (f (n + 1))) ∧ (∀ (n : ℕ), Valid (f n)) ∧ Filter.Tendsto (fun (n : ℕ) => (f n).1 + (f n).2) Filter.atTop Filter.atTop

Let $G$ be the graph with vertex set those pairs $(x,y)\in \mathbb{N}^2$ with $\mathrm{gcd}(x,y)=1$, in which we join two vertices if the differ in only one coordinate, and there by $\pm 1$.

Is there a path going to infinity on $G$, say $P$, such that for all $(x,y)\in P$ both $\min(x,y)>1$ and at least one of $x$ or $y$ is composite?

The weaker version (only $\min(x,y) > 1$) was solved by C. Stewart via the prime-pair path $(p_k, p_{k+1}) \to (p_{k+1}, p_{k+2})$, as recounted in [Er80]; the compositeness condition forbids those anchors and the question is open.

theorem Erdos1212.vertical_leg_valid {a b c : ℕ} (ha : a.Composite) (hb : 2 ≤ b) (hV : ∀ (s : ℕ), b ≤ s → s ≤ c → a.gcd s = 1) (s : ℕ) : b ≤ s → s ≤ c → Valid (a, s)

Core of the composite-anchor reduction: vertical-leg vertices $(a, s)$ for $b \le s \le c$ are valid vertices of the strengthened problem, given the anchor $a$ is composite and coprime to the whole leg.

theorem Erdos1212.horizontal_leg_valid {a b c : ℕ} (hc : c.Composite) (ha2 : 2 ≤ a) (hH : ∀ (s : ℕ), a ≤ s → s ≤ b → s.gcd c = 1) (s : ℕ) : a ≤ s → s ≤ b → Valid (s, c)

Core of the composite-anchor reduction: horizontal-leg vertices $(s, c)$ for $a \le s \le b$ are valid, given the anchor $c$ is composite and coprime to the whole leg.

theorem Erdos1212.anchor_coprime_of_short_leg {a s : ℕ} (hs : a < s) (h : ∀ (p : ℕ), Nat.Prime p → p ∣ a → s < a + p) : a.gcd s = 1

Roughness criterion (sufficiency for the anchor conditions): if $a < s$ for all $s$ in the leg and the leg stays below $a + P^-(a)$, then $a$ is coprime to the whole leg. Stated via divisibility: no prime factor of $a$ divides any $s$ with $a < s < a + p$ for all prime factors $p$ of $a$.

theorem Erdos1212.right_neighbor_witness_free {P : Finset ℕ} {x y : ℕ} (hP : ∀ p ∈ P, Nat.Prime p) (hx : ∀ p ∈ P, p ∣ x) (hy : ∀ p ∈ P, ¬p ∣ y) (p : ℕ) : p ∈ P → ¬p ∣ x + 1 ∧ ¬p ∣ y

Isolation lemma, right neighbour (core of the no-periodic-certificate theorem): if every prime in $P$ divides $x$ and none divides $y$, then no prime of $P$ divides either coordinate of $(x+1, y)$.

theorem Erdos1212.left_neighbor_witness_free {P : Finset ℕ} {x y : ℕ} (hP : ∀ p ∈ P, Nat.Prime p) (hx1 : 1 ≤ x) (hx : ∀ p ∈ P, p ∣ x) (hy : ∀ p ∈ P, ¬p ∣ y) (p : ℕ) : p ∈ P → ¬p ∣ x - 1 ∧ ¬p ∣ y

Isolation lemma, left neighbour.

theorem Erdos1212.vertical_neighbor_both_even {x y : ℕ} (h2x : 2 ∣ x) (h2y : ¬2 ∣ y) : (2 ∣ x ∧ 2 ∣ y + 1) ∧ (1 ≤ y → 2 ∣ x ∧ 2 ∣ y - 1)

Isolation lemma, vertical neighbours: both coordinates even.