---

Claim. The manuscript "Infinite paths in the composite-restricted visible lattice" claims that the subgraph of $G$ induced on the coprime pairs $(x,y)$ with $\min(x,y)>1$ and $x$ or $y$ composite contains an infinite simple path, the affirmative answer to Problem 1212, and more: for Lebesgue-almost every $\alpha\in(4/3,5/3)$ there is such a path $(x_n,y_n)$ with $x_n/y_n\to\alpha$. The tab entry's outline: a localized bad crossing is associated with an integer polynomial of bounded height, large common prime divisors force an evaluation of that polynomial to vanish, summable estimates on the exceptional directions give safe crossings in narrowing corridors, and connecting the crossings across dyadic scales and extracting a simple ray gives the path and its limiting direction; the record's abstract adds a Jacobsthal bound for finding composite supporting columns and planar crossing duality with overlapping rectangles. The summary follows the tab entry and the record's abstract.

Submission note. Posted to erdosproblems.com as a proof claim by Alex Chengyu Li (account alexchengyuli) on 7 September 2026, giving "Proof Engine (https://doi.org/10.2139/ssrn.7237460; https://doi.org/10.5281/zenodo.22346064), with ChatGPT 5.6 and ChatGPT 6 Astra" as the AI used:

I prove that the composite-restricted visible lattice contains an infinite simple path, answering Problem 1212 affirmatively. More precisely, for Lebesgue-almost every $\alpha\in(4/3,5/3)$, there is such a path with $x_n/y_n\to\alpha$. The key step associates a bounded-height integer polynomial to a localized bad crossing, using large common prime divisors to force a polynomial evaluation to vanish. Summable exceptional-direction estimates then give safe crossings in narrowing corridors. Connecting these crossings across dyadic scales and extracting a simple ray gives the claimed infinite path and limiting direction. Notes: Formalization was completed after the linked Zenodo version. The original problem and the displayed main theorem are kernel-checked in Lean using only propext, Classical.choice and Quot.sound. The linked public repository contains the formalization, current manuscript, audit output and versioned release v1.0.0.

Standing. Alex Chengyu Li published the manuscript on Zenodo on 6 September 2026 and filed the claim on the site's proof-claims tab on 7 September 2026, whose tools line names a system called Proof Engine, with SSRN and Zenodo records of its own, together with ChatGPT 5.6 and ChatGPT 6 Astra. The Zenodo concept record (doi:10.5281/zenodo.22448686, linked above) holds four versions: 1.0.0 and 1.0.1 of 6 September 2026 (03:12 and 03:21 UTC), 1.0.2 of 7 September 2026 and 1.0.3 of 8 September 2026, the last with a new file, erdos1212_algebraic_corridors.pdf; the tab's link is version 1.0.1. The Zenodo text of version 1.0.1 says that the proofs had not yet been formalized and that formal verification was planned; the tab entry says that the formalization was completed after that version, and the 1.0.3 abstract announces a public Lean 4 formalization whose recorded kernel audit reports only propext, Classical.choice and Quot.sound. The 1.0.3 abstract also credits rafalwrona's mixed-modulus determinant observation in the site's thread (23 August 2026) as sharing the local arithmetic mechanism of the proof's interpolation step, and Ephraim Duncan's drift and finite-path observations there (21 July 2026), says that these observations do not supply the global infinite-path construction, and says that the mathematical statements and proofs are unchanged from the earlier versions. The tab entry carries no comments, the site's label is unchanged (OPEN; page last edited 08 April 2026), and as of 2026-10-07 the claim has no refereed publication or outside review. The claim stays claimed.

Lean. The repository linked above, pinned at its head commit of 7 September 2026 (the fourth of four commits), describes itself as a Lean 4 formalization of the manuscript's result, says that the problem's statement and the displayed main theorem are checked with only propext, Classical.choice and Quot.sound, carries a kernel-audit file and the recorded kernel output, and says that this is machine verification and not a claim of journal peer review; the repository page shows the release v1.0.1 (the tab entry names v1.0.0). The repository's first commit, of 14 July 2026, holds a different and earlier paper, titled as a machine-certified closure of the problem and resting on computation certified outside Lean; the README at the pinned commit calls the history before the release superseded private staging material that is not part of the release's mathematical evidence, so the claimant does not present it as evidence and it has no page of its own. This corpus has not built or audited the development, so no formalized evidence is listed.

Depends on. Nothing on the wiki.