Erdős problem 1212 · problems.science

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$ .

Sources

Browse retained paths and inspect the exact material available for this Problem.

8 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1212.lean

Retained formal statement7 of 8

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.

FormalConjectures/ErdosProblems/1212.leanErdos1212.vertical_leg_valid2 linesExact file

1∀ {a b c : ℕ},2  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

Sources

Search problems.science