ProofAtlas research outcome
Strong Papadimitriou–Ratajczak Conjecture
The paper, exact Lean statements, checked evidence, and immutable source release are collected on the canonical formalization page.
Result boundary
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.
Independent acceptance review is not complete.