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

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

FormalConjectures/ErdosProblems/1212.leanErdos1212.right_neighbor_witness_free1 lineExact file

1∀ {P : Finset ℕ} {x y : ℕ}, (∀ p ∈ P, Nat.Prime p) → (∀ p ∈ P, p ∣ x) → (∀ p ∈ P, ¬p ∣ y) → ∀ p ∈ P, ¬p ∣ x + 1 ∧ ¬p ∣ y

APIStatement only, no proof

Sources

Search problems.science