Bigeodesics in planar first-passage percolation
From OpenAI Aftermath
Bigeodesics in planar first-passage percolation are doubly infinite paths that minimize passage time between any two of their vertices; the planar no-bigeodesics conjecture, a question attributed to Furstenberg by Kesten, asserts that they almost surely do not exist for independent continuous edge weights on Z2. Two manuscripts in OpenAI's public mathematics collection (github.com/openai/math), both dated 24 September 2026, claim the conjecture when the minimum of four weights has a finite second moment, and claim that the limit shape for exponential weights is strictly convex with C1 boundary, differentiability holding for every Gamma law. The collection includes a Lean formalization of the differentiability statements only. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introductions of the manuscripts:
- First-passage percolation was introduced by Hammersley and Welsh. Infinite geodesics and Busemann functions were developed by Newman, Hoffman, and Damron and Hanson; Licea and Newman proved coalescence in almost every direction and excluded bigeodesics with prescribed end directions in that set, and Damron and Hanson obtained exclusions in fixed sectors under differentiability assumptions on the limit shape and state the conjecture.
- Wehr and Woo excluded bigeodesics in the half-plane, with moment conditions later removed by Auffinger, Damron and Hanson; Brito, Damron and Hanson excluded doubly infinite paths in certain limiting geodesic graphs, and Alexander excluded all bigeodesics under exponential-moment, curvature and fluctuation assumptions. Ahlberg and Hoffman developed a structural theory that assigns an asymptotically linear Busemann function to every ray without shape assumptions; the manuscript uses it as its structural input.
- The fine geometry of the limit shape is much harder to determine than its existence, as surveyed by Auffinger, Damron and Hanson, and strict convexity and differentiability were conjectured for the planar exponential model. Lalley gave sufficient conditions for strict convexity, Durrett and Liggett found a flat edge in Richardson's growth model, Marchand determined flat segments for laws with an atom at their positive minimum, and Auffinger and Damron proved differentiability at the endpoints of such segments.
The original results
- Claim. Theorem 1.1 of No bigeodesics in planar first-passage percolation states that for independent edge weights with a common law without atoms, such that the minimum of four independent weights has a finite second moment, almost surely no doubly infinite nearest-neighbour path minimizes passage time between all of its vertices; no assumption on the limit shape is made, and the moment-free formulation is not asserted. Theorem 1.1 of Strict convexity and differentiability of the planar exponential first-passage limit shape states that for exponential weights the time-constant norm is differentiable away from the origin and its unit ball is strictly convex, so that the boundary is a C1 curve with a unique supporting line at every point; Theorem 1.2 states differentiability for Gamma weights of every shape and rate.
- Method, as described: the no-bigeodesics manuscript labels each ray by the linear asymptote of its Busemann function, deals separately with the environment-dependent exceptional labels for which uniqueness for fixed labels does not apply, and derives a contradiction from a finite budget for passage-time increases on a grid, together with a fork-counting argument in the style of Burton and Keane.
- Sources. The manuscripts No bigeodesics in planar first-passage percolation and Strict convexity and differentiability of the planar exponential first-passage limit shape at commit
1581d4c. - Formalization, as described by the repository. The scope note states that the formalization proves differentiability of the time-constant norm away from the origin, with a C1 boundary of the unit ball, for Gamma edge weights of every positive shape and rate, including a unique supporting line at every boundary point in the exponential case; strict convexity is outside the selected statements. The scope note does not mention bigeodesics. The Comparator statements are
PlanarFirstPassage.leanandGammaPassage.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 20 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "partial": the primary claim, the absence of bigeodesics, is not stated, nor is strict convexity of the exponential limit shape; the stated results are the differentiability statements for exponential and Gamma weights. It records sandboxed Comparator passes for PlanarFirstPassage and GammaPassage. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 | cert-machine, openai/math lane K, run 38040214623: PlanarFirstPassage and GammaPassage | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept both solutions, in 505 s and 513 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. | Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) lists neither challenge, so both were accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-13 | M. Colbrook and contributors, AIM — Open Applied Problems (GitHub), problem 171 | Catalogue | The collection records its problem 171, the absence of bigeodesics for mean-one exponential weights, as solved by the no-bigeodesics manuscript, noting that exponential weights satisfy its moment hypothesis and that the linked Lean scope covers only differentiability of limit shapes. | The status review is described as "an AI statement-level review of a published manuscript, not a fresh independent audit of its complete proof or a Lean kernel replay". The collection is not affiliated with the American Institute of Mathematics. |
| 2026-10-16 | J. Jardine, Lattice24, referee review of the no-bigeodesics manuscript in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap and states that the reviewer read every section line by line. Its two minor notes are that the argument uses the structural theorems of Ahlberg and Hoffman as a black box, which the reviewer did not check against the source and calls a dependency rather than a gap, and that the appendix replacing a boundary-expectation step of Ahlberg and Hoffman reuses two geometric parts of their paper, the rest of which the reviewer re-derived. | Part of an audit of the collection's manuscripts without Lean that the audit describes as complete. The reviews are published under CC BY 4.0. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscripts.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
