A conjecture open since 2004 is now a theorem, checked in Lean

Lech Mazur@LechMazur

The strong Papadimitriou–Ratajczak conjecture, open since 2004, is now a theorem: every 3-connected planar graph admits a convex greedy drawing. The proof was found using the t.co/Qc8LLe9Jjx harness and GPT-6 Pro and is formalized in Lean (52k lines).

Greedy routing forwards a message to a neighboring vertex that is closer to its destination. A greedy drawing guarantees that such a neighbor exists at every step, so the message eventually arrives. Using virtual coordinates, this requires only local neighbor information and the destination's coordinates. The strong conjecture requires this property together with straight edges, no crossings and convex faces.

A graph is 3-connected if it has at least four vertices and remains connected after removing any one or two vertices. For 3-connected planar graphs, progress went from greedy drawings to planar greedy drawings to convex greedy drawings:

2004 — Papadimitriou and Ratajczak propose the weak and strong conjectures. The weak version allows crossings; the strong version requires a planar drawing with convex faces.

2008 — Leighton and Moitra, and independently Angelini, Frati and Grilli, prove the weak conjecture: every 3-connected planar graph admits a greedy drawing. Their drawings can have crossing edges.

2017 — Da Lozzo, D’Angelo and Frati establish the planar version: greedy drawings with no crossing edges, but not necessarily convex faces.

2026 — The new proof establishes the convex version, for any prescribed outer face, with every facial polygon strictly convex.

The construction first assigns distinct integer heights so that, for every destination, every other vertex has a neighbor whose height is strictly closer to the destination's height. The horizontal coordinates are then chosen within a narrow vertical strip to produce a convex drawing. The strip is narrow enough that the vertical improvement dominates, so Euclidean distance decreases too.

Paper: t.co/nmac6XtB9v

Lean formalization: