Is there an infinite composite-coordinate path in the visible-lattice-point graph? (Erdős #1212)
Statement
Let $G$ be the graph whose vertices are the visible lattice points, i.e. the pairs $(x,y)\in\mathbb{N}^2$ with $\gcd(x,y)=1$, where two vertices are joined by an edge if they differ in exactly one coordinate and there by $\pm 1$. Is there a path $P$ in $G$ that goes to infinity such that every vertex $(x,y)\in P$ satisfies both $\min(x,y)>1$ and at least one of $x,y$ is composite?
Acceptance. FULLY RESOLVES: a complete proof (Lean/Coq preferred, else a full written proof) that an infinite constrained path exists — e.g. an explicit construction scheme together with a proof it continues forever while keeping every vertex coprime, with $\min(x,y)>1$ and a composite coordinate — OR a proof that no such infinite path exists (e.g. that the constrained induced subgraph has only finite components in the relevant region). ADVANCES: a reproducible computational construction of a constrained path reaching a record maximum coordinate $N$, delivered as the explicit vertex sequence plus a checker verifying that each consecutive pair is a legal edge of $G$ and each vertex satisfies coprimality, $\min>1$, and the composite-coordinate condition (state the attained $N$; this is evidence, since reaching infinity requires proof); OR a proof resolving the monotone / bounded-turn variant; OR a proof that the constrained subgraph has an infinite component. Deliver the proof, or the path data plus verifier plus attained $N$.
Background
Posed by Erdős [Er80, p.114]. The graph $G$ of visible lattice points was studied by Herzog and Stewart, who proved it has a single infinite connected component and conjectured that $(a,p)$ lies in that component whenever $p$ is prime and $p\nmid a$ (Bloom notes he could not locate this precise result in Herzog–Stewart's published work [HeSt71], which concerns which finite patterns occur among visible lattice points). Erdős originally asked the weaker question with only the constraint $\min(x,y)>1$ and, as he recounts in [Er80], 'foolishly offered 25 dollars for a proof'; that evening Stewart gave a simple argument, joining $(p_k,p_{k+1})$ to $(p_{k+1},p_{k+2})$ via the path $(p_k,p_{k+1})\to(p_k,p_{k+1}+1)\to\cdots\to(p_k,p_{k+2})\to(p_k+1,p_{k+2})\to(p_{k+1},p_{k+2})$, which is legal provided $[p_{k+1},p_{k+2}]$ contains no multiple of $p_k$ — true whenever $p_{k+2}<2p_k$, i.e. for all $k\geq 4$. The present, still-open question strengthens the constraint to also require a composite coordinate at every step. Erdős further asks for a monotone path (each step increasing the distance from the origin) that changes direction after only a bounded number of steps. A formalised statement exists in google-deepmind/formal-conjectures (FormalConjectures/ErdosProblems/1212.lean). Listed as open on erdosproblems.com/1212 (fetched 2026-07-21, status 'open'); the current question carries no prize (the \$25 was for the weaker, already-solved version). The attacker's tool: graph search — enumerate the visible lattice points, restrict to vertices with $\min(x,y)>1$ and a composite coordinate, and run BFS/DFS on the induced subgraph to map its infinite component and drive a constrained path as far out as possible, testing the monotone / bounded-turn variant computationally.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #1212 (T. F. Bloom) | website |
| REF-02 | Lean formalisation of Erdős #1212 (formal-conjectures) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.