Strict convexity and differentiability of the planar exponential first-passage limit shape

Lean formalization in OpenAI math repository (Result 212)

Model / AI: OpenAI (unreleased)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'Strict convexity and differentiability of the planar exponential first-passage limit shape'. We prove that the limit shape of undirected nearest-neighbor first-passage percolation on ℤ2 with independent exponential edge weights is strictly convex and has a C1 boundary. This resolves the strict convexity and differentiability conjectures for the planar exponential model. More generally, we prove differentiability of the time-constant norm for every Gamma edge-weight law with positive shape and rate.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 212). The Lean development was not rebuilt locally.

• Paper — Paper
• Lean — Lean formalization note
• Code — OpenAI math repository