OpenAI claim summary for Math-1736
mathematicsTop Open Problemscontributionliterature_reportClaim: literature report
Summary of a claim published in openai/math; not a claim by this platform.
The cited theorem gives strict convexity and C1 differentiability of the planar exponential shape, but our question asks its explicit directional norm in every d>=2; neither a formula nor the other dimensions is determined. This entry records partial support; complete coverage of the question is not established by this catalogue.
Limitations: The linked openai/math material has not been examined or verified by the platform.
Manuscript
Contents
Limit shape of first-passage percolation
OpenAI's claim
OpenAI presents a mathematical result relevant to this question in the selected manuscript. The exponential planar first-passage shape is claimed to be strictly convex with a continuously differentiable boundary; Gamma laws are also claimed to give differentiable time constants.Mathematical statement of the claimed result
Result 1.
For nearest-neighbor first-passage percolation on $\mathbb Z^2$ with independent exponential weights of fixed rate $\lambda>0$, let $\mu$ denote the time-constant norm and $\mathcal B=\{x:\mu(x)\le1\}$. The source claims differentiability of $\mu$ on $\mathbb R^2\setminus\{0\}$, a $C^1$ boundary of $\mathcal B$, and \[ x,y\in\partial\mathcal B,\ x\ne y,\ 0<t<1 \quad\Longrightarrow\quad\mu((1-t)x+ty)<1. \] Thus its unit ball is strictly convex and has one supporting line at each boundary point. This theorem is for exponential weights, not arbitrary passage laws.Outline of the argument
The argument separates the removal of corners from the removal of flat faces. Busemann and geodesic comparisons establish differentiability for Gamma weights, while an additional exponential-law argument excludes linear boundary segments; the two conclusions are then combined.Formal verification
For family 212, the documented entries give differentiability and continuously differentiable boundaries for planar Gamma shapes, including the exponential law. They do not supply strict convexity or the separate no-bigeodesic theorem. The listed Comparator files areGammaPassage.lean, PlanarFirstPassage.lean. Named declarations include OAI.PlanarFPP.manuscriptMain. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.Status caveat
OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.Sources
- OpenAI, Strict convexity and differentiability of the planar exponential first-passage limit shape, 2026-09-24; citation key
OAI:Strict-convexity-and-differentiability-of-the-planar-exponential-first-passage-limit-shape-September-24-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:exponential-shape. - Family 212: Lean scope.
- Comparator GammaPassage.json.
- Comparator GammaPassage.lean.
- Comparator PlanarFirstPassage.json.
- Comparator PlanarFirstPassage.lean.
- OpenAI catalogue entry.