VibeMathedMath problems solved with AI
Sign in

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

For i.i.d. edge weights on Z2\mathbb Z^2, the Cox-Durrett shape theorem gives a norm μ\mu with T(0,⌊tv⌋)/t→μ(v)T(0,\lfloor tv\rfloor)/t\to\mu(v) and a convex limit shape B={μ≤1}\mathcal B=\{\mu\le1\}. It is conjectured that for continuous weight laws B\mathcal B is strictly convex (no flat faces) and that μ\mu is differentiable away from the origin (no corners); see the survey of Auffinger, Damron and Hanson. Neither property was known for any continuous law, including the exponential law, where the model coincides with the Eden-Richardson growth model. Partial results covered laws with an atom at the minimum (Marchand; Auffinger-Damron) and sufficient conditions (Lalley). For i.i.d. exponential edge weights, is the limit shape strictly convex with a C1C^1 boundary?

Result
Proved(see note)
Status
Partial result
AI contribution
AI-discovered
Method
Argument
Field
First-passage percolation; limit shapes
Posed by
Open questions surveyed by Auffinger, Damron and Hanson (50 years of first-passage percolation, 2017)
Year posed
2017
Years open
9y
Solved
2026-09-24
Model
Unreleased internal OpenAI model
Vendor
OpenAI
Collaborators
—
Verification
Lean-checked, statement unaudited
Publication
Announced
Collection
OpenAI math release (October 2026), version adc7f12
Significance
38 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Theorem 1.1: for i.i.d. exponential weights of any rate, μ\mu is Frechet differentiable on R2∖{0}\mathbb R^2\setminus\{0\} and B\mathcal B is strictly convex, so ∂B\partial\mathcal B is a C1C^1 curve with a unique supporting line at each point. Theorem 1.2: differentiability (not strict convexity) holds for every Gamma law with positive shape and rate. Consequences for directional geodesics and Busemann functions follow from Damron-Hanson. It does not treat general continuous laws, higher dimensions, or curvature of the boundary.

What the AI did

The release README says the vast majority of results, this one included, were produced with one fixed procedure using an unreleased internal OpenAI model, on average about three hours of ChatGPT Pro thinking compute per result, and that some outputs build on earlier model results. This result is not among the README's exceptions (the Hodge conjecture for CM abelian varieties and the Re(s) > 11/12 zero-free region, whose write-up was human-edited). The manuscript is authored 'OpenAI' and names no human author.

Verification

No independent mathematician has checked this yet. Checked here: Theorems 1.1 and 1.2 were read against the conjectures; they settle the exponential law (strict convexity and differentiability) and differentiability for Gamma laws, special cases of the general conjectures, hence Partial. The proof was not refereed. lean/formalization.yaml lists OAI.PlanarFPP.manuscriptMain (comparator PlanarFirstPassage). Its statement was read: for i.i.d. Exp(1) weights there is a norm that is the almost-sure time constant, differentiable away from 0, with unique normalized supporting functionals, a C1C^1 unit sphere, a unique supporting line and a C1C^1 chart at every boundary point. A second challenge, GammaPassage.json (OAI.GammaFPP.gamma_differentiability, solution module OAI.Probability.GammaPassage.Differentiability, present at the pinned commit), is not in the formalization catalogue; read here, it states the same differentiability for every Gamma(shape, rate) law. Strict convexity is not formalized. Not rebuilt here.

Sources

Changelog1 change

Discussion