Immutable source snapshot
Strong Papadimitriou–Ratajczak Conjecture source at 2469f1b840e8
This permanent route identifies the exact Git snapshot used by the recorded Lean theorem. The complete checked import closure, source footprint, downloads, and checker evidence are available on the source page.
Git commit2469f1b840e839355c948371bf614f5155349270
Recorded theorem endpoint
StrongPR.strong_pr_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.