A route through every planar network may become greedy
- What it is
- A paper and Lean package claim every finite 3-connected plane graph has a convex drawing that supports greedy routing.
- Who did it
- Lech Mazur, with ProofAtlas-reported contributions from OpenAI Codex and OpenAI GPT-6 Pro
- What it could mean
- A long-standing graph-drawing question may gain an exact machine-checkable endpoint, while the crucial comparison between that code and the companion paper remains open.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
A Proof of the Strong Papadimitriou–Ratajczak Conjecture ↗See the proposed checks
In a separate ephemeral environment, source-lock the disclosed Lean commit; reproduce its build and unfinished-proof/axiom checks; then independently compare the formal theorem’s original-drawing hypotheses and conclusion with the companion paper’s stated strong conjecture.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
- What it claims
- The exact declaration constructs a straight-line embedding with strict convex face cycles and a neighboring vertex closer to every distinct destination, under an original-drawing and deletion-connectivity formulation of finite simple 3-connected plane graphs.
- Why this could matter
- A route through every planar network may become greedy In a greedy drawing, each hop toward a destination gets strictly closer. This release claims every sufficiently well-connected planar network can be drawn that way, while keeping the proof’s exact scope and independent review visible.
- If it holds up
- It would settle the stated strong graph-drawing conjecture and provide a formal endpoint for studying convex greedy-routing constructions.
- If it does not
- A mismatch between the Lean statement, its assumptions, or the paper’s claimed theorem would identify the boundary needing repair; the conjecture would remain open.
- Impact horizon
- Methods · Graph theory · Computational geometry · Formal verification
- Version
- public version of 2026-09-09; companion paper is 15 pages; Lean package reports 499 first-party files and a pinned build evidence record.
- Why we tracked it
- This older-than-72-hours release was newly surfaced by the current Reddit discovery channel and independently inspected at its primary formalization page. It supplies both a precise theorem declaration and explicit limits rather than a social claim alone.
- Highest-risk dependency
- Lean verification applies to the exact declaration, not automatically to every sentence of the paper or its historical claim. The source explicitly leaves paper-to-statement alignment, independent replication, specialist review, and accepted-result status open.
- Available artifacts
- ProofAtlas exposes a public pinned Lean source package, a checker-evidence JSON record, a source ZIP, a main Lean file, and the companion PDF. No manuscript, source package, or checker was downloaded, executed, or replayed.
- Current boundary
- Intake record only; examination not started.