/- 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).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 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 ∣ 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 ∣ 1this:1 < p⊢ 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 ∣ 1this✝:1 < pthis:p = 1⊢ False 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 ∣ 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 - 1h1:p ∣ 1this:1 < p⊢ 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 ∣ 1this✝:1 < pthis:p = 1⊢ 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