Erdős problem 1212
Let be the graph with vertex set those pairs with , in which we join two vertices if the differ in only one coordinate, and there by .
Sources
FormalConjectures/ErdosProblems/
1212.lean
Retained formal statement
Let be the graph with vertex set those pairs with , in which we join two vertices if the differ in only one coordinate, and there by .
Is there a path going to infinity on , say , such that for all both and at least one of or is composite?
The weaker version (only ) was solved by C. Stewart via the prime-pair path , as recounted in [Er80]; the compositeness condition forbids those anchors and the question is open.
True ↔ ∃ f, 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.atTopOpenStatement only, no proof