SIGNIFICANCE

Checked 2026-09-08 · source current · v1

Alex Chengyu Li · ErdősProblems.com #1212

What is claimed?

We prove that this graph contains an infinite simple path, answering Erdős Problem 1212 affirmatively. More precisely, for almost every slope in a fixed interval away from the diagonal, there is a ray with that limiting coordinate ratio.

Quoted from the source · Significance editor · 2026-09-08 §Abstract, p.1 · View source

Component dates
Preprint
2026-09-07
Exposition
Not recorded
Formalization
2026-09-07

Component dates (preprint / exposition / formalization). Formalization date from the artifact reported by the source. “Not recorded” means no dated source is recorded for that component. Preprint dates refer to the pinned manuscript version.

Reader summary

Claimed
Alex Chengyu Li reports an infinite simple path in the composite-restricted visible lattice and an almost-everywhere limiting-direction result. The author selected release v1.0.1 for this private draft.

Reader summary · Significance · 2026-09-08

What has been checked?

Significance inspected the problem and claim pages, repository links, and pinned v1.0.1 version; resolved the tag to a commit; and computed the manuscript PDF SHA-256 from the raw file at that commit.

Reader summary · Significance · 2026-09-08

Independent reruns
0
Math assessments
0
Written reviews
0

Where is help needed?

The mathematics has not been independently assessed. Significance has not reproduced the Lean build or established statement correspondence. The author-supplied correspondence task and independent verification remain open.

Reader summary · Significance · 2026-09-08

Open questions contributed by Alex Chengyu Li.

  • Correspondence: Compare the graph and path conditions in Section 1, Problem 1212, Target.lean, and AlgebraicCorridorKernelAudit.lean.

    Check composite-coordinate restrictions, unit adjacency, and the implication from an injective infinite path to a path going to infinity. Record discrepancies and unresolved questions. Allow...

See 1 open check →

Problem link

ErdősProblems.com #1212 · open the original problem page

Quoted from the source · Significance editor · 2026-09-08 · View source

Author involvement

The author contributed a suggested review task. Private correspondence is not reproduced.

Record note · alexchengyuli · 2026-09-08

Start here · for reviewers

Main deduction

Compare Section 1's graph and path conditions with Problem 1212, Target.lean, and the literal endpoint in AlgebraicCorridorKernelAudit.lean.

Section 1; Target.lean; AlgebraicCorridorKernelAudit.lean · Significance’s interpretation · Significance editor · 2026-09-08 §Private correspondence; message text withheld.

Risk points

  • Check that the composite-coordinate restriction and unit adjacency agree across the problem, paper, and named Lean statements.

    Graph and path conditions · Significance’s interpretation · Significance editor · 2026-09-08 §Private correspondence; message text withheld.

  • Check the passage from the injective infinite path to the original question's path going to infinity.

    Injectivity and the original existence question · Significance’s interpretation · Significance editor · 2026-09-08 §Private correspondence; message text withheld.

Useful background

  • Section 1 of the paper, the repository README, and the two named Lean files; familiarity with reading Lean statements.

    Significance’s interpretation · Significance editor · 2026-09-08 §Private correspondence; message text withheld.

Needs checking

  • List the statements and conditions compared and any specific discrepancy or remaining question within the author's bounded correspondence check.

    First task: statement correspondence · Significance’s interpretation · Significance editor · 2026-09-08 §Private correspondence; message text withheld.

  • Suggest another focused check

Formalization handoff

A compact map for someone who wants to formalize this claim. It records preparation and open work, not a mathematical verdict.

Target
The graph and path conditions in Problem 1212, Target.lean, and the literal endpoint in AlgebraicCorridorKernelAudit.lean. Significance’s interpretation · Significance editor · 2026-09-08 §Private correspondence; message text withheld.
System
Lean 4 Quoted from the source · Significance editor · 2026-09-08 · View source
Work state
Artifact reported
Code
formalization repository · commit 400001f0847a…

Paper/code correspondence: The formal artifact is author-reported and has not been independently reproduced. Its correspondence with the problem and paper remains the author's first open task. Significance’s interpretation · Significance editor · 2026-09-08 §Private correspondence; message text withheld.

Stated by the author · alexchengyuli · 2026-09-08 §Private correspondence; message text withheld.

Copy for sharing

Copy and paste this summary.

Alex Chengyu Li reports an infinite simple path in the composite-restricted
visible lattice and an almost-everywhere limiting-direction result. The
author selected release v1.0.1 for this private draft.

Checked: Significance inspected the problem and claim pages, repository
links, and pinned v1.0.1 version; resolved the tag to a commit; and computed
the manuscript PDF SHA-256 from the raw file at that commit.

Not checked: The mathematics has not been independently assessed.
Significance has not reproduced the Lean build or established statement
correspondence. The author-supplied correspondence task and independent
verification remain open.

As of 2026-09-08T14:30:26Z (freshness: current)
Full record: https://hjyuh.github.io/significance/2026-alexchengyuli-erdos-1212/
Significance records evidence. It does not judge the mathematics.
Scope
This private draft concerns the author's claimed infinite path in the composite-restricted visible lattice and the author-selected v1.0.1 release. The optional monotonicity and bounded-turn strengthening is outside the reported scope. Statement correspondence and independent mathematical assessment remain open. Significance’s interpretation · Significance editor · 2026-09-08 · View source
Source
Infinite paths in the composite-restricted visible lattice · github-crabsatellite-erdos-1212-400001f0847afe36a26c588d34445210dbdc116e · retrieved 2026-09-08T14:23:09Z
sha256 2a31595c68dd…

Evidence: 6 entries

  1. Source inspection

    ev-source-inspection

    Public-source and version check only. This is not a mathematical review.

    Significance inspected the public problem and proof-claim pages and their source links, located the pinned manuscript version, and computed its SHA-256 from the downloaded PDF bytes. The mathematics has not been independently assessed; the author-supplied task remains open.

    Significance’s interpretation · Significance editor · 2026-09-08 · View source

  2. Source inspection

    ev-ai-claim-disclosure

    Public-source and version check only. This is not a mathematical review.

    A full proof claimed by Alex Chengyu Li (using Proof Engine (doi.org/… doi.org/… with ChatGPT 5.6 and ChatGPT 6 Astra).

    Quoted from the source · Significance editor · 2026-09-08 · View source

  3. Source inspection

    ev-version-pin

    Public-source and version check only. This is not a mathematical review.

    The author-selected tag v1.0.1 resolves to commit 400001f0847a…. manuscript.url is the raw PDF at that commit; its SHA-256 is 2a31595c68dd…, computed from 283837 downloaded bytes at 2026-09-08T14:23:09Z. The claim page still names v1.0.0; the author's later message selects v1.0.1.

    Significance’s interpretation · Significance editor · 2026-09-08 · View source

  4. Formal code published by the source

    ev-formalization-reported

    Published by the source. Any independent rerun appears as a separate entry.

    The specific Problem 1212 proof claim links this Lean repository as its formalization. The pinned v1.0.1 release was published on 2026-09-07 and includes the manuscript, Lean sources, and audit material. This records a published artifact, not an independent reproduction.

    Open link @ 400001f0847a… · Significance’s interpretation · Significance editor · 2026-09-07 §Published release; linked formalization in Erdős Problems proof claim 278 · View source

  5. Source inspection

    ev-author-first-task

    Public-source and version check only. This is not a mathematical review.

    Editorial summary of the author-suggested task: Compare the graph and path conditions in Section 1, Problem 1212, Target.lean, and AlgebraicCorridorKernelAudit.lean. Check composite-coordinate restrictions, unit adjacency, and the implication from an injective infinite path to a path going to infinity. Record discrepancies and unresolved questions. Allow approximately 1–2 hours for this statement comparison.

    Significance’s interpretation · Significance editor · 2026-09-08 §Private correspondence; message text withheld.

  6. Source inspection

    ev-publication-date

    Public-source and version check only. This is not a mathematical review.

    The pinned v1.0.1 release containing this manuscript was published on 2026-09-07. This dates the pinned manuscript release, not its earliest circulation.

    Significance’s interpretation · Significance editor · 2026-09-09 · View source

Limits of this record
  • This record does not issue a whole-paper correctness judgement.
  • Open invitations identify work not yet represented by a completed evidence entry.
  • No independent reproduction or mathematical assessment is represented unless an evidence entry above says otherwise.