/- 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 Filternamespace 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 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 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 < aValid (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 < a1 < (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 < a1 < (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 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 < cValid (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 < c1 < (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 < c1 < (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 sFalse 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)$.

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 1False 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 < pFalse 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 = 1False All goals completed! 🐙

Isolation lemma, left neighbour.

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 1False 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 < pFalse 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 = 1False 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