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 .
Mathematical 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.
Statement source: Erdős Problems statement material
Statement terms: Source-specific
Source-specific terms. Therefore does not assert reuse rights beyond attributed display.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
erdos_1212
theorem erdos_1212 : answer(sorry) ↔ ∃ f : ℕ → ℕ × ℕ, Function.Injective f ∧ (∀ n, Adj (f n) (f (n + 1))) ∧ (∀ n, Valid (f n)) ∧ Tendsto (fun n => (f n).1 + (f n).2) atTop atTop := by sorry- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References