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 statement1 of 8

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

FormalConjectures/ErdosProblems/1212.leanErdos1212.anchor_coprime_of_short_leg1 lineExact file

1∀ {a s : ℕ}, a < s → (∀ (p : ℕ), Nat.Prime p → p ∣ a → s < a + p) → a.gcd s = 1

APIStatement only, no proof

Sources

Search problems.science