Erdős problem 1212

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

The source's own material, retained exactly.

8 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1212.lean

Retained formal statement6 of 8

Sanity check for Valid: the vertex $(4, 3)$ is valid — both coordinates exceed $1$ , they are coprime, and $4$ is composite.

FormalConjectures/ErdosProblems/1212.leanErdos1212.valid_four_three1 lineExact file

1Erdos1212.Valid (4, 3)

TestStatement only, no proof