Skip to content

Erdős problem 1212

Let GG be the graph with vertex set those pairs (x,y)∈N2(x,y)\in \mathbb{N}^2 with gcd(x,y)=1\mathrm{gcd}(x,y)=1, in which we join two vertices if the differ in only one coordinate, and there by ±1\pm 1.

Sources

The source's own material, retained exactly.

8 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1212.lean

Retained formal statement7 of 8

Core of the composite-anchor reduction: vertical-leg vertices (a,s)(a, s) for b≤s≤cb \le s \le c are valid vertices of the strengthened problem, given the anchor aa is composite and coprime to the whole leg.

FormalConjectures/ErdosProblems/1212.leanErdos1212.vertical_leg_valid2 linesExact file
∀ {a b c : ℕ},  a.Composite → 2 ≤ b → (∀ (s : ℕ), b ≤ s → s ≤ c → a.gcd s = 1) → ∀ (s : ℕ), b ≤ s → s ≤ c → Erdos1212.Valid (a, s)
APIStatement only, no proof