Formal evidence
An independent reviewer must inspect the recorded build, declarations, unfinished-proof-step check, and disclosed foundations.
ProofAtlas research case study
Starting frontierStrong Papadimitriou–Ratajczak conjecture→AI-developed Lean-checked candidatePaper + pinned Lean existence theorem
Evidence and status →Graph drawing · geometric routing · formal theorem
Strong Papadimitriou–Ratajczak Conjecture
A paper and pinned Lean package give a proof candidate that every finite simple 3-connected plane graph has a convex greedy straight-line drawing preserving its prescribed embedding and outer face.
Scope: Every finite simple 3-connected plane graph, presented by an original continuous plane drawing, has a straight-line drawing that preserves its embedding and outer face, has strictly convex facial polygons, and admits a strictly closer adjacent step toward every distinct destination; the construction records a Euclidean decrease of at least 3/4 in its normalization.
Lean checkedRecorded build passed
Unfinished proof stepsNone
PublicationReview pending
Exact formal proposition
Hypotheses and conclusion
theorem strong_pr_conjecture
(hd : IsOriginalDrawing G Finset.univ p arc)
(hcard : 4 ≤ (Finset.univ : Finset V).card)
(hcuts : ∀ X : Finset V, X.card ≤ 2 → ConnectedOn G (Finset.univ \ X)) :
∃ (q : V → Plane)
(F : List (NativeFaceBoundary G))
(_ : IsNativeFaceFamily Finset.univ arc (mappedOriginalGraph G Finset.univ p) F)
(o : {f : NativeFaceBoundary G // f ∈ F})
(bodies : {f : NativeFaceBoundary G // f ∈ F} → Set Plane)
(H : Plane ≃ₜ Plane),
Function.Injective q
∧ IsOriginalDrawing G Finset.univ q (originalStraightArc q)
∧ (∀ s t : V, s ≠ t → ∃ a, G.Adj s a ∧ dist (q t) (q a) + 3 / 4 ≤ dist (q t) (q s))
∧ (∀ s t : V, s ≠ t → ∃ a, G.Adj s a ∧ 1 ≤ dist (q t) (q s)^2 - dist (q t) (q a)^2)
∧ (∀ (d : G.Dart) (v : V), q v ∈ segment ℝ (q d.fst) (q d.snd) ↔ v = d.fst ∨ v = d.snd)
∧ (∀ d e : G.Dart, d.edge ≠ e.edge → segment ℝ (q d.fst) (q d.snd) ∩ segment ℝ (q e.fst) (q
e.snd) = q '' (({d.fst, d.snd} : Set V) ∩ {e.fst, e.snd}))
∧ ¬Bornology.IsBounded o.val.region
∧ (∀ f : {f : NativeFaceBoundary G // f ∈ F}, IsStrictConvexCycle q (if f = o then
f.val.walk.reverse else f.val.walk) (bodies f))
∧ (∀ f : {f : NativeFaceBoundary G // f ∈ F}, H '' f.val.region = if f = o then (bodies f)ᶜ
else interior (bodies f))
∧ (∀ (f : {f : NativeFaceBoundary G // f ∈ F}) z, z ∈ (if f = o then (bodies f)ᶜ else
interior (bodies f)) → originalFace G Finset.univ q (originalStraightArc q) z = if f = o
then (bodies f)ᶜ else interior (bodies f))
∧ (∀ v : V, H (p v) = q v)
∧ (∀ (d : G.Dart) (t : unitInterval), H (hd.dartPath d (Finset.mem_univ _) (Finset.mem_univ
_) t) = Path.segment (q d.fst) (q d.snd) t)
∧ (∀ (η : C(unitInterval, Plane)) (hη : η 1 = η 0) (x : Plane) (hx : ∀ t, η t ≠ x),
planeLoopWinding ((H : C(Plane, Plane)).comp η) (congrArg H hη) (H x) (fun t he => hx t
(H.injective he)) = planeLoopWinding η hη x hx)
∧ ∀ d : G.Dart, IsStraightClockwiseSuccessor Finset.univ q d (nativeVertexPermutation F d)Result boundary
What this theorem does—and does not—establish
Every finite simple 3-connected plane graph, presented by an original continuous plane drawing, has a straight-line drawing that preserves its embedding and outer face, has strictly convex facial polygons, and admits a strictly closer adjacent step toward every distinct destination; the construction records a Euclidean decrease of at least 3/4 in its normalization.
- The checked endpoint does not independently certify every sentence, citation, or historical statement in the companion paper.
- ProofAtlas accepted-result status, independent statement alignment, specialist peer review, historical priority, and unrelated replication remain open.
- The source release's internal acceptance record is source-project evidence and does not confer ProofAtlas accepted-result status.
- The supplied infographic and dark homepage cover are explanatory images, not proof or formal-verification evidence.
- The disclosed Lean foundations are standard logical foundations, not graph-theoretic or geometric assumptions.
Companion research paper
A Proof of the Strong Papadimitriou–Ratajczak Conjecture
The September 9 paper proves that every finite simple 3-connected plane graph admits a convex greedy straight-line drawing preserving its prescribed embedding and outer face. An accompanying Lean 4 development checks the existence theorem from the original continuous plane drawing and three-connectivity assumptions.
Author-authorized early release. This fixed paper package first appeared while independent presentation review was pending; hosting it does not mark the Lean result accepted.
Paper, rights, and source relationship
Hosting authorized by the rightsholder. ProofAtlas metadata cover; not a reproduction of a paper page or part of the proof.
Lech Mazur, “A Proof of the Strong Papadimitriou–Ratajczak Conjecture,” September 9, 2026.
- The primary Lean endpoint starts from the original continuous plane drawing and deletion-connectivity assumptions and constructs the straight-line drawing, facial bodies, ambient homeomorphism, strict convexity, rotation preservation, and normalized greedy margins. The paper states the conventional finite simple 3-connected plane-graph theorem; independent ProofAtlas paper-to-formal-statement alignment review remains open.
- The retained source release reports successful fresh public checks, exact source and dependency inventories, no admissions, and the standard foundation closure propext, Classical.choice, and Quot.sound. ProofAtlas reran the headline checker under its local cap on September 10, but no ProofAtlas accepted-result record has been created.
- The source release also exposes the stronger declaration StrongPR.strong_pr_prescribed_outer_edge. This publication records the main existence declaration as its formal evidence page and publishes the full immutable source tree for inspection.
- Neither the paper nor the Lean record independently establishes historical priority, specialist peer review, or unrelated replication.
Paper overview
The strong Papadimitriou–Ratajczak conjecture and convex greedy routing
Author-supplied explanation of the theorem, a representative dodecahedral drawing, the greedy routing rule, and the proof ingredients. It is explanatory, not proof or formal-verification evidence.
Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.
Continue the mathematics
Open questions and extensions
The pinned theorem and its complete local import closure let people and AI agents inspect the proof, compare another route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks each proposed extension against its own exact statement.
What the source ZIP contains
The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled.
Formal theorem publication status
Publication review
Accepted-result publication remains pending
Lean has checked the exact source; this public release is not presented as a ProofAtlas accepted result. The linked evidence page shows individual review decisions where they are publicly available. The requirements below describe publication coverage, not a count of unfinished reviews. Independent AI, human, or mixed reviewers may examine the build evidence, statement alignment, result boundary, and public wording. Review does not replace Lean's check or broaden the theorem.
Statement alignment
The formal declaration must be reviewed against the theorem wording and its exact variant.
Result boundary
The limits must be checked so the page cannot imply a broader theorem.
Public wording
The explanation, infographic labels, and source presentation need independent review.
Canonical source
The permanent source link and downloadable files must be approved for public citation.
Accepted result
After the four reviews and source route are ready, an accepted-result record must bind them to this exact formalization.
Credit for this release
Contributors and roles
Authorship and other contributions are recorded separately for this version.
Contributions
- Direct contributionOpenAI Codex, OpenAI GPT-6 Pro
OpenAI GPT-6 Pro and OpenAI Codex have source-reported roles in mathematical exploration, proof development, computational testing, Lean formalization, and exposition.
- Computation
- Exposition
- Formalization
- Proof strategy
- Direct contributionLech Mazur
Lech Mazur is the paper author, accountable editor, and research director for the Strong Papadimitriou–Ratajczak result.
- Exposition
- Proof strategy
- Research direction
Citation
Cite this release
Use the version-specific citation so the authorship, scope, and public record remain attached.
Release history
Versions and public record
- Release
- Paper release
- Version
- public version of September 9, 2026
- Published
- Canonical page
- Open canonical page
Release chronology
This version is part of the release history. No independent external timestamp is claimed.
Scope of this release
- No ProofAtlas accepted-result record exists for the Strong Papadimitriou–Ratajczak artifact in this snapshot.
- No independent external priority anchor, specialist peer review, unrelated replication, or independent statement-alignment review is recorded.
- The paper, source ZIP, supplied infographic, and ProofAtlas covers are authorized for ProofAtlas distribution but have no general open-content license.
- The public Lean source is separately Apache-2.0 licensed at its rights commit; Mathlib, Schoenflies, and cited third-party works retain their own rights.
- The source release's internal acceptance record does not confer ProofAtlas accepted-result status.