/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilErdős Problem 1212
References:
[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.
open Filternamespace Erdos1212A vertex of the strengthened problem: a visible lattice point with both coordinates exceeding 1 and at least one coordinate composite.
def Valid (p : ℕ × ℕ) : Prop :=
1 < p.1 ∧ 1 < p.2 ∧ Nat.gcd p.1 p.2 = 1 ∧ (¬ p.1.Prime ∨ ¬ p.2.Prime)
Sanity check for Valid: the vertex $(4, 3)$ is valid — both coordinates exceed $1$,
they are coprime, and $4$ is composite.
@[category test, AMS 11]
theorem valid_four_three : Valid (4, 3) := ⊢ Valid (4, 3)
⊢ 1 < (4, 3).1⊢ 1 < (4, 3).2⊢ (4, 3).1.gcd (4, 3).2 = 1⊢ ¬Nat.Prime (4, 3).1 ∨ ¬Nat.Prime (4, 3).2 ⊢ 1 < (4, 3).1⊢ 1 < (4, 3).2⊢ (4, 3).1.gcd (4, 3).2 = 1⊢ ¬Nat.Prime (4, 3).1 ∨ ¬Nat.Prime (4, 3).2 All goals completed! 🐙Two lattice points are adjacent iff they differ by exactly 1 in exactly one coordinate.
def Adj (p q : ℕ × ℕ) : Prop :=
(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))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.
@[category research open, AMS 11]
theorem erdos_1212 :
answer(sorry) ↔ ∃ f : ℕ → ℕ × ℕ, Function.Injective f ∧ (∀ n, Adj (f n) (f (n + 1))) ∧
(∀ n, Valid (f n)) ∧
Tendsto (fun n => (f n).1 + (f n).2) atTop atTop := ⊢ True ↔
∃ f,
Function.Injective f ∧
(∀ (n : ℕ), Adj (f n) (f (n + 1))) ∧ (∀ (n : ℕ), Valid (f n)) ∧ Tendsto (fun n ↦ (f n).1 + (f n).2) atTop atTop
All goals completed! 🐙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.
@[category API, AMS 11]
theorem vertical_leg_valid {a b c : ℕ} (ha : a.Composite) (hb : 2 ≤ b)
(hV : ∀ s, b ≤ s → s ≤ c → Nat.gcd a s = 1) :
∀ s, b ≤ s → s ≤ c → Valid (a, s) := a:ℕb:ℕc:ℕha:a.Compositehb:2 ≤ bhV:∀ (s : ℕ), b ≤ s → s ≤ c → a.gcd s = 1⊢ ∀ (s : ℕ), b ≤ s → s ≤ c → Valid (a, s)
a:ℕb:ℕc:ℕha:a.Compositehb:2 ≤ bhV:∀ (s : ℕ), b ≤ s → s ≤ c → a.gcd s = 1s:ℕhs1:b ≤ shs2:s ≤ c⊢ Valid (a, s)
a:ℕb:ℕc:ℕha:a.Compositehb:2 ≤ bhV:∀ (s : ℕ), b ≤ s → s ≤ c → a.gcd s = 1s:ℕhs1:b ≤ shs2:s ≤ cha2:1 < a⊢ Valid (a, s)
exact ⟨a:ℕb:ℕc:ℕha:a.Compositehb:2 ≤ bhV:∀ (s : ℕ), b ≤ s → s ≤ c → a.gcd s = 1s:ℕhs1:b ≤ shs2:s ≤ cha2:1 < a⊢ 1 < (a, s).1 All goals completed! 🐙, a:ℕb:ℕc:ℕha:a.Compositehb:2 ≤ bhV:∀ (s : ℕ), b ≤ s → s ≤ c → a.gcd s = 1s:ℕhs1:b ≤ shs2:s ≤ cha2:1 < a⊢ 1 < (a, s).2 All goals completed! 🐙, hV s hs1 hs2, Or.inl ha.2⟩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.
@[category API, AMS 11]
theorem horizontal_leg_valid {a b c : ℕ} (hc : c.Composite) (ha2 : 2 ≤ a)
(hH : ∀ s, a ≤ s → s ≤ b → Nat.gcd s c = 1) :
∀ s, a ≤ s → s ≤ b → Valid (s, c) := a:ℕb:ℕc:ℕhc:c.Compositeha2:2 ≤ ahH:∀ (s : ℕ), a ≤ s → s ≤ b → s.gcd c = 1⊢ ∀ (s : ℕ), a ≤ s → s ≤ b → Valid (s, c)
a:ℕb:ℕc:ℕhc:c.Compositeha2:2 ≤ ahH:∀ (s : ℕ), a ≤ s → s ≤ b → s.gcd c = 1s:ℕhs1:a ≤ shs2:s ≤ b⊢ Valid (s, c)
a:ℕb:ℕc:ℕhc:c.Compositeha2:2 ≤ ahH:∀ (s : ℕ), a ≤ s → s ≤ b → s.gcd c = 1s:ℕhs1:a ≤ shs2:s ≤ bhc2:1 < c⊢ Valid (s, c)
exact ⟨a:ℕb:ℕc:ℕhc:c.Compositeha2:2 ≤ ahH:∀ (s : ℕ), a ≤ s → s ≤ b → s.gcd c = 1s:ℕhs1:a ≤ shs2:s ≤ bhc2:1 < c⊢ 1 < (s, c).1 All goals completed! 🐙, a:ℕb:ℕc:ℕhc:c.Compositeha2:2 ≤ ahH:∀ (s : ℕ), a ≤ s → s ≤ b → s.gcd c = 1s:ℕhs1:a ≤ shs2:s ≤ bhc2:1 < c⊢ 1 < (s, c).2 All goals completed! 🐙, hH s hs1 hs2, Or.inr hc.2⟩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$.
a:ℕs:ℕhs:a < sh:∀ (p : ℕ), Nat.Prime p → p ∣ a → s < a + phg:¬a.gcd s = 1p:ℕhp:Nat.Prime phpd:p ∣ a.gcd shlt:s < a + pk:ℕhk:a = p * kl:ℕhl:s = p * lhp0:0 < phkl:k < lthis✝:p * (k + 1) ≤ p * lthis:a + p ≤ s⊢ False
omega All goals completed! 🐙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)$.
@[category API, AMS 11]
theorem right_neighbor_witness_free {P : Finset ℕ} {x y : ℕ} (hP : ∀ p ∈ P, p.Prime)
(hx : ∀ p ∈ P, p ∣ x) (hy : ∀ p ∈ P, ¬ p ∣ y) :
∀ p ∈ P, ¬ p ∣ (x + 1) ∧ ¬ p ∣ y := by P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ y⊢ ∀ p ∈ P, ¬p ∣ x + 1 ∧ ¬p ∣ y
intro p hp P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ P⊢ ¬p ∣ x + 1 ∧ ¬p ∣ y
refine ⟨fun hdvd => ?_, hy p hp⟩ P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x + 1⊢ False
have h1 : p ∣ 1 := by P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ y⊢ ∀ p ∈ P, ¬p ∣ x + 1 ∧ ¬p ∣ y P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x + 1h1:p ∣ 1⊢ False
have h := Nat.dvd_sub hdvd (hx p hp) P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x + 1h:p ∣ x + 1 - x⊢ p ∣ 1 P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x + 1h1:p ∣ 1⊢ False
simpa using h P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x + 1h1:p ∣ 1⊢ False P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x + 1h1:p ∣ 1⊢ False
have := (hP p hp).one_lt P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x + 1h1:p ∣ 1this:1 < p⊢ False
have := Nat.dvd_one.mp h1 P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x + 1h1:p ∣ 1this✝:1 < pthis:p = 1⊢ False
omega All goals completed! 🐙Isolation lemma, left neighbour.
@[category API, AMS 11]
theorem left_neighbor_witness_free {P : Finset ℕ} {x y : ℕ} (hP : ∀ p ∈ P, p.Prime)
(hx1 : 1 ≤ x) (hx : ∀ p ∈ P, p ∣ x) (hy : ∀ p ∈ P, ¬ p ∣ y) :
∀ p ∈ P, ¬ p ∣ (x - 1) ∧ ¬ p ∣ y := by P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ y⊢ ∀ p ∈ P, ¬p ∣ x - 1 ∧ ¬p ∣ y
intro p hp P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ P⊢ ¬p ∣ x - 1 ∧ ¬p ∣ y
refine ⟨fun hdvd => ?_, hy p hp⟩ P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x - 1⊢ False
have h1 : p ∣ 1 := by P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ y⊢ ∀ p ∈ P, ¬p ∣ x - 1 ∧ ¬p ∣ y P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x - 1h1:p ∣ 1⊢ False
have h := Nat.dvd_sub (hx p hp) hdvd P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x - 1h:p ∣ x - (x - 1)⊢ p ∣ 1 P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x - 1h1:p ∣ 1⊢ False
have hx_sub : x - (x - 1) = 1 := by P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ y⊢ ∀ p ∈ P, ¬p ∣ x - 1 ∧ ¬p ∣ y P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x - 1h:p ∣ x - (x - 1)hx_sub:x - (x - 1) = 1⊢ p ∣ 1 P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x - 1h1:p ∣ 1⊢ False omega P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x - 1h:p ∣ x - (x - 1)hx_sub:x - (x - 1) = 1⊢ p ∣ 1 P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x - 1h1:p ∣ 1⊢ False P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x - 1h:p ∣ x - (x - 1)hx_sub:x - (x - 1) = 1⊢ p ∣ 1 P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x - 1h1:p ∣ 1⊢ False
rwa [hx_sub P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x - 1h:p ∣ 1hx_sub:x - (x - 1) = 1⊢ p ∣ 1 P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x - 1h1:p ∣ 1⊢ False] P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x - 1h:p ∣ 1hx_sub:x - (x - 1) = 1⊢ p ∣ 1 P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x - 1h1:p ∣ 1⊢ False at h P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x - 1h1:p ∣ 1⊢ False
have := (hP p hp).one_lt P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x - 1h1:p ∣ 1this:1 < p⊢ False
have := Nat.dvd_one.mp h1 P:Finset ℕx:ℕy:ℕhP:∀ p ∈ P, Nat.Prime phx1:1 ≤ xhx:∀ p ∈ P, p ∣ xhy:∀ p ∈ P, ¬p ∣ yp:ℕhp:p ∈ Phdvd:p ∣ x - 1h1:p ∣ 1this✝:1 < pthis:p = 1⊢ False
omega All goals completed! 🐙Isolation lemma, vertical neighbours: both coordinates even.
@[category API, AMS 11]
theorem vertical_neighbor_both_even {x y : ℕ} (h2x : 2 ∣ x) (h2y : ¬ 2 ∣ y) :
(2 ∣ x ∧ 2 ∣ (y + 1)) ∧ (1 ≤ y → 2 ∣ x ∧ 2 ∣ (y - 1)) := by x:ℕy:ℕh2x:2 ∣ xh2y:¬2 ∣ y⊢ (2 ∣ x ∧ 2 ∣ y + 1) ∧ (1 ≤ y → 2 ∣ x ∧ 2 ∣ y - 1)
refine ⟨⟨h2x, by x:ℕy:ℕh2x:2 ∣ xh2y:¬2 ∣ y⊢ 2 ∣ y + 1 omega All goals completed! 🐙⟩, fun hy1 => ⟨h2x, by x:ℕy:ℕh2x:2 ∣ xh2y:¬2 ∣ yhy1:1 ≤ y⊢ 2 ∣ y - 1 omega All goals completed! 🐙⟩⟩end Erdos1212