/- 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 FormalConjecturesUtil

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.

open Filter namespace Erdos1212

A 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).11 < (4, 3).2(4, 3).1.gcd (4, 3).2 = 1¬Nat.Prime (4, 3).1 ¬Nat.Prime (4, 3).2 1 < (4, 3).11 < (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 declaration uses 'sorry'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 ss 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 cValid (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.leftValid (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.left1 < (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.left1 < (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 ss 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 bValid (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.leftValid (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.left1 < (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.left1 < (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 + pa.gcd s = 1 a:s:hs:a < sh: (p : ), Nat.Prime p p a s < a + phg:¬a.gcd s = 1False 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 = 1a.gcd s 1 a:s:hs:a < sh: (p : ), Nat.Prime p p a s < a + phg:¬a.gcd s = 1h1:a.gcd s = 1False 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 hpaFalse -- 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 * kFalse 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 * lFalse 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 hpFalse have hkl : k < l := a:s:hs:a < sh: (p : ), Nat.Prime p p a s < a + pa.gcd s = 1 have : p * k < p * l := a:s:hs:a < sh: (p : ), Nat.Prime p p a s < a + pa.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 hklFalse have : a + p s := a:s:hs:a < sh: (p : ), Nat.Prime p p a s < a + pa.gcd s = 1 have hpk : p * (k + 1) = a + p := a:s:hs:a < sh: (p : ), Nat.Prime p p a s < a + pa.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 hklp * (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 + 1False 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 h1False 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 - 1False 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) hdvdp 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) = 1p 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 h1False 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 y2 y + 1 All goals completed! 🐙, fun hy1 => h2x, x:y:h2x:2 xh2y:¬2 yhy1:1 y2 y - 1 All goals completed! 🐙 end Erdos1212