Skip to content

Erdős problem 1212

Start work

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

Isolation lemma, right neighbour (core of the no-periodic-certificate theorem): if every prime in PP divides xx and none divides yy, then no prime of PP divides either coordinate of (x+1,y)(x+1, y).

FormalConjectures/ErdosProblems/1212.leanErdos1212.right_neighbor_witness_free1 lineExact file
∀ {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