/-
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
[Er80] Erdős, P.,
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 Filter
namespace 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)
intro s a:ℕb:ℕc:ℕha:a.Compositehb:2 ≤ bhV:∀ (s : ℕ), b ≤ s → s ≤ c → a.gcd s = 1s:ℕhs1: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 := ha.left⊢ 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 := ha.left⊢ 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 := ha.left⊢ 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)
intro s a:ℕb:ℕc:ℕhc:c.Compositeha2:2 ≤ ahH:∀ (s : ℕ), a ≤ s → s ≤ b → s.gcd c = 1s:ℕhs1: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 := hc.left⊢ 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 := hc.left⊢ 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 := hc.left⊢ 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$.
@[category API, AMS 11]
theorem anchor_coprime_of_short_leg {a s : ℕ} (hs : a < s)
(h : ∀ p, p.Prime → p ∣ a → s < a + p) : Nat.gcd a s = 1 := a:ℕs:ℕhs:a < sh:∀ (p : ℕ), Nat.Prime p → p ∣ a → s < a + p⊢ a.gcd s = 1
a:ℕs:ℕhs:a < sh:∀ (p : ℕ), Nat.Prime p → p ∣ a → s < a + phg:¬a.gcd s = 1⊢ False
obtain ⟨p, hp, hpd⟩ := Nat.exists_prime_and_dvd (n := Nat.gcd a s) (a:ℕs:ℕhs:a < sh:∀ (p : ℕ), Nat.Prime p → p ∣ a → s < a + phg:¬a.gcd s = 1⊢ a.gcd s ≠ 1
a:ℕs:ℕhs:a < sh:∀ (p : ℕ), Nat.Prime p → p ∣ a → s < a + phg:¬a.gcd s = 1h1:a.gcd s = 1⊢ False
All goals completed! 🐙)
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 shpa:p ∣ a := Dvd.dvd.trans hpd (Nat.gcd_dvd_left a s)⊢ False
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 shpa:p ∣ a := Dvd.dvd.trans hpd (Nat.gcd_dvd_left a s)hps:p ∣ s := Dvd.dvd.trans hpd (Nat.gcd_dvd_right a s)⊢ False
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 shpa:p ∣ a := Dvd.dvd.trans hpd (Nat.gcd_dvd_left a s)hps:p ∣ s := Dvd.dvd.trans hpd (Nat.gcd_dvd_right a s)hlt:s < a + p := h p hp hpa⊢ False
-- s is a multiple of p strictly between a (a multiple of p) and a + p: impossible
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 shps:p ∣ s := Dvd.dvd.trans hpd (Nat.gcd_dvd_right a s)hlt:s < a + p := h p hp hpak:ℕhk:a = p * k⊢ False
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 + p := h p hp hpak:ℕhk:a = p * kl:ℕhl:s = p * l⊢ False
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 + p := h p hp hpak:ℕhk:a = p * kl:ℕhl:s = p * lhp0:0 < p := Nat.Prime.pos hp⊢ False
have hkl : k < l := a:ℕs:ℕhs:a < sh:∀ (p : ℕ), Nat.Prime p → p ∣ a → s < a + p⊢ a.gcd s = 1
have : p * k < p * l := a:ℕs:ℕhs:a < sh:∀ (p : ℕ), Nat.Prime p → p ∣ a → s < a + p⊢ a.gcd s = 1 All goals completed! 🐙
All goals completed! 🐙
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 + p := h p hp hpak:ℕhk:a = p * kl:ℕhl:s = p * lhp0:0 < p := Nat.Prime.pos hphkl:k < l :=
have this := Decidable.byContradiction fun a_1 => anchor_coprime_of_short_leg._proof_1 hs p k hk l hl a_1;
Nat.lt_of_mul_lt_mul_left thisthis:p * (k + 1) ≤ p * l := Nat.mul_le_mul_left p hkl⊢ False
have : a + p ≤ s := a:ℕs:ℕhs:a < sh:∀ (p : ℕ), Nat.Prime p → p ∣ a → s < a + p⊢ a.gcd s = 1
have hpk : p * (k + 1) = a + p := a:ℕs:ℕhs:a < sh:∀ (p : ℕ), Nat.Prime p → p ∣ a → s < a + p⊢ a.gcd s = 1 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 + p := h p hp hpak:ℕhk:a = p * kl:ℕhl:s = p * lhp0:0 < p := Nat.Prime.pos hphkl:k < l :=
have this := Decidable.byContradiction fun a_1 => anchor_coprime_of_short_leg._proof_1 hs p k hk l hl a_1;
Nat.lt_of_mul_lt_mul_left thisthis:p * (k + 1) ≤ p * l := Nat.mul_le_mul_left p hkl⊢ p * (k + 1) = p * k + p; All goals completed! 🐙
All goals completed! 🐙
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 := 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 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
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 := 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 + 1h:p ∣ x + 1 - x := Nat.dvd_sub hdvd (hx p hp)⊢ p ∣ 1
All goals completed! 🐙
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 :=
have h := Nat.dvd_sub hdvd (hx p hp);
Eq.mpr (id Nat.dvd_one._simp_1)
(Eq.mp (Eq.trans (congrArg (Dvd.dvd p) (add_tsub_cancel_left x 1)) Nat.dvd_one._simp_1) h)this:1 < p := Nat.Prime.one_lt (hP p hp)⊢ 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 :=
have h := Nat.dvd_sub hdvd (hx p hp);
Eq.mpr (id Nat.dvd_one._simp_1)
(Eq.mp (Eq.trans (congrArg (Dvd.dvd p) (add_tsub_cancel_left x 1)) Nat.dvd_one._simp_1) h)this✝:1 < p := Nat.Prime.one_lt (hP p hp)this:p = 1 := Nat.dvd_one.mp h1⊢ False
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 := 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 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
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 := 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) := Nat.dvd_sub (hx p hp) hdvd⊢ p ∣ 1
have hx_sub : x - (x - 1) = 1 := 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 All goals completed! 🐙
rwa [hx_subP: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 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 :=
have h := Nat.dvd_sub (hx p hp) hdvd;
have hx_sub := Decidable.byContradiction fun a => left_neighbor_witness_free._proof_1 hx1 p a;
Eq.mp (congrArg (fun _a => p ∣ _a) hx_sub) hthis:1 < p := Nat.Prime.one_lt (hP p hp)⊢ 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 - 1h1:p ∣ 1 :=
have h := Nat.dvd_sub (hx p hp) hdvd;
have hx_sub := Decidable.byContradiction fun a => left_neighbor_witness_free._proof_1 hx1 p a;
Eq.mp (congrArg (fun _a => p ∣ _a) hx_sub) hthis✝:1 < p := Nat.Prime.one_lt (hP p hp)this:p = 1 := Nat.dvd_one.mp h1⊢ False
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)) := x:ℕy:ℕh2x:2 ∣ xh2y:¬2 ∣ y⊢ (2 ∣ x ∧ 2 ∣ y + 1) ∧ (1 ≤ y → 2 ∣ x ∧ 2 ∣ y - 1)
refine ⟨⟨h2x, x:ℕy:ℕh2x:2 ∣ xh2y:¬2 ∣ y⊢ 2 ∣ y + 1 All goals completed! 🐙⟩, fun hy1 => ⟨h2x, x:ℕy:ℕh2x:2 ∣ xh2y:¬2 ∣ yhy1:1 ≤ y⊢ 2 ∣ y - 1 All goals completed! 🐙⟩⟩
end Erdos1212