Skip to content

Erdős problem 1212

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

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

8 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1212.lean

Retained formal statement2 of 8

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.

Is there a path going to infinity on GG, say PP, such that for all (x,y)P(x,y)\in P both min(x,y)>1\min(x,y)>1 and at least one of xx or yy is composite?

The weaker version (only min(x,y)>1\min(x,y) > 1) was solved by C. Stewart via the prime-pair path (pk,pk+1)(pk+1,pk+2)(p_k, p_{k+1}) \to (p_{k+1}, p_{k+2}), as recounted in [Er80]; the compositeness condition forbids those anchors and the question is open.

FormalConjectures/ErdosProblems/1212.leanErdos1212.erdos_12125 linesExact file
Truef,    Function.Injective f      (∀ (n : ℕ), Erdos1212.Adj (f n) (f (n + 1))) ∧        (∀ (n : ℕ), Erdos1212.Valid (f n)) ∧ Filter.Tendsto (fun n => (f n).1 + (f n).2) Filter.atTop Filter.atTop
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page