# Planar first-passage geometry and the absence of bigeodesics > Planar random-metric grids are claimed to have no route that is fastest forever both ways, and a smooth limit shape. Canonical: https://closedform.nishachay.tech/e/openai-math-2026-212/ Last updated: 2026-10-14 **Planar random-metric grids are claimed to have no route that is fastest forever both ways, and a smooth limit shape.** **Trust:** Formal proof listed · **Papers:** 2 · **First paper:** September 24, 2026 · **Field:** Probability and statistical mechanics · **Entry:** 212 *Explained by AI.* Drafted by one AI model and checked sentence by sentence against the paper by a different one. Spot a mistake? Report an error. Give each road of a square grid a random travel time and measure distance by the fastest route. One paper claims that no route is fastest forever in both directions, under a mild moment condition. The other studies the large-scale shape of the reachable region. For exponential travel times it claims the shape has no flat edges and no corners. Lean has a formal proof of the no-corners part, for every Gamma law. ## At a glance - **First step:** 1965 (John Hammersley and Dominic Welsh, first-passage percolation) - **Significance:** Major. It would settle two long-standing planar conjectures, one of them with a partial Lean proof. - **Trust:** Formal proof listed - **Field:** Probability and statistical mechanics (2 papers) ## The explanation Picture a square grid of roads. Each road segment has its own random travel time. Take one small square of four segments. Going right then up costs 0.5 + 0.4 = 0.9 hours. Going up then right costs 0.2 + 0.9 = 1.1 hours. So the fastest time between opposite corners is 0.9 hours, along the first route. This is first-passage percolation: a random grid whose distance is the fastest travel time[1]. A fastest route is called a geodesic. Now make the grid infinite. Over long distances, travel time grows in proportion to the distance, but at different rates in different directions. The set of points reachable within time t, shrunk by a factor of t, settles into a fixed convex shape[2]. This is the limit shape. Its exact form is unknown even for simple weights. For exponential travel times, its fine geometry was a long-open question[3]. Two papers address this setting. The first asks about routes that are fastest in both directions forever. Such a route is called a bigeodesic. The question goes back to Furstenberg, as recorded by Kesten[4]. The conjecture says that, for continuous random weights, no bigeodesic exists[5]. The first paper claims to prove this, with one condition[6]. The smallest of four independent weights must have finite average square[6]. It rules out all bigeodesics at once, with no assumption on the limit shape[7]. The second paper looks at the limit shape itself, for exponential weights. Two things could make the shape irregular. A flat edge is a straight piece of boundary. A corner is a point where the boundary has more than one tangent line[8]. The paper claims the shape has neither: it is strictly convex and its boundary is smooth, a C¹ curve[9]. It also proves smoothness for every Gamma law of weights, a wider family that includes the exponential[10]. Earlier results came with assumptions. Newman showed that routes have directions, but needed curvature of the shape and an extra moment condition[11]. Damron and Hanson excluded some bigeodesics, but needed the shape to be smooth in places[12]. Licea and Newman excluded bigeodesics only for directions chosen in advance[13]. The single obstacle was that every method needed some regularity of the unknown shape. The first paper removes that need. Its argument handles every possible direction at once. How sure is this? A computer proof checker called Lean has a formal proof that the shape's boundary is smooth. It covers every Gamma law of weights, including the exponential one. Strict convexity of the exponential shape lies outside that check. So does the absence of bigeodesics. No specialist review of either paper has been published. **What it doesn't show.** This does not give a formula for the limit shape, or remove the moment condition from the no-bigeodesics result. ## Where it came from This result comes from an unreleased OpenAI model, published in the openai/math release on 6 October 2026. ## Hype check Major if it holds. Smoothness of the shape for Gamma weights has a Lean proof; strict convexity and the no-bigeodesics result do not. No specialist review is published. ## Words used - **First-passage percolation:** A grid with random travel times on its edges, where distance is the fastest total travel time. - **Geodesic:** A fastest route between two points. - **Bigeodesic:** A path, infinite in both directions, every piece of which is a fastest route. - **Limit shape:** The convex shape that the region reachable within time t approaches after shrinking by t. - **Strictly convex:** Having no straight pieces on the boundary. - **C¹ boundary:** A boundary with a single tangent line at every point, so no corners. - **Gamma law:** A family of probability laws for positive numbers that includes the exponential law. ## The original papers (2) - [No bigeodesics in planar first-passage percolation](https://github.com/openai/math/blob/main/preprints/No-bigeodesics-in-planar-first-passage-percolation-September-24-2026/main.pdf) - September 24, 2026 - [Strict convexity and differentiability of the planar exponential first-passage limit shape](https://github.com/openai/math/blob/main/preprints/Strict-convexity-and-differentiability-of-the-planar-exponential-first-passage-limit-shape-September-24-2026/main.pdf) - September 24, 2026 · Formal proof listed - [Lean notes](https://github.com/openai/math/blob/main/lean/docs/212.md) ## Quoted lines from the paper (13) [1] From [No bigeodesics in planar first-passage percolation](https://github.com/openai/math/blob/main/preprints/No-bigeodesics-in-planar-first-passage-percolation-September-24-2026/main.pdf): > First-passage percolation, introduced by Hammersley and Welsh, equips a lattice with a random metric by assigning independent passage times to its edges. [2] From [Strict convexity and differentiability of the planar exponential first-passage limit shape](https://github.com/openai/math/blob/main/preprints/Strict-convexity-and-differentiability-of-the-planar-exponential-first-passage-limit-shape-September-24-2026/main.pdf): > Its unit ball $\Bcal=\{v:\mu(v)\le1\}$ is the limit shape. [3] From [Strict convexity and differentiability of the planar exponential first-passage limit shape](https://github.com/openai/math/blob/main/preprints/Strict-convexity-and-differentiability-of-the-planar-exponential-first-passage-limit-shape-September-24-2026/main.pdf): > Although the shape theorem gives a convex deterministic body, its fine geometry is much harder to determine; see the survey of Auffinger, Damron, and Hanson. [4] From [No bigeodesics in planar first-passage percolation](https://github.com/openai/math/blob/main/preprints/No-bigeodesics-in-planar-first-passage-percolation-September-24-2026/main.pdf): > The question was attributed to Furstenberg by Kesten. [5] From [No bigeodesics in planar first-passage percolation](https://github.com/openai/math/blob/main/preprints/No-bigeodesics-in-planar-first-passage-percolation-September-24-2026/main.pdf): > The planar no-bigeodesics conjecture asserts that bigeodesics are absent for iid continuous edge-weight laws; see. [6] From [No bigeodesics in planar first-passage percolation](https://github.com/openai/math/blob/main/preprints/No-bigeodesics-in-planar-first-passage-percolation-September-24-2026/main.pdf): > We prove the conjecture under the minimum-of-four second-moment assumption. [7] From [No bigeodesics in planar first-passage percolation](https://github.com/openai/math/blob/main/preprints/No-bigeodesics-in-planar-first-passage-percolation-September-24-2026/main.pdf): > We assume no differentiability, strict convexity, or curvature of the limit shape. [8] From [Strict convexity and differentiability of the planar exponential first-passage limit shape](https://github.com/openai/math/blob/main/preprints/Strict-convexity-and-differentiability-of-the-planar-exponential-first-passage-limit-shape-September-24-2026/main.pdf): > Strict convexity and differentiability exclude different features of a convex boundary: a flat face has more than one point on a supporting line, whereas a corner has more than one supporting line at a point (Figure …). [9] From [Strict convexity and differentiability of the planar exponential first-passage limit shape](https://github.com/openai/math/blob/main/preprints/Strict-convexity-and-differentiability-of-the-planar-exponential-first-passage-limit-shape-September-24-2026/main.pdf): > We prove that the limit shape of undirected nearest-neighbor first-passage percolation on $\Z^2$ with independent exponential edge weights is strictly convex and has a $C^1$ boundary. [10] From [Strict convexity and differentiability of the planar exponential first-passage limit shape](https://github.com/openai/math/blob/main/preprints/Strict-convexity-and-differentiability-of-the-planar-exponential-first-passage-limit-shape-September-24-2026/main.pdf): > More generally, we prove differentiability of the time-constant norm for every Gamma edge-weight law with positive shape and rate. [11] From [No bigeodesics in planar first-passage percolation](https://github.com/openai/math/blob/main/preprints/No-bigeodesics-in-planar-first-passage-percolation-September-24-2026/main.pdf): > The complementary assertion that every ray has a direction and that rays exist in every direction was established by Newman under an exponential moment and uniform curvature. [12] From [No bigeodesics in planar first-passage percolation](https://github.com/openai/math/blob/main/preprints/No-bigeodesics-in-planar-first-passage-percolation-September-24-2026/main.pdf): > Damron and Hanson subsequently obtained one-end exclusions in fixed tangent-contact sectors under local differentiability assumptions. [13] From [No bigeodesics in planar first-passage percolation](https://github.com/openai/math/blob/main/preprints/No-bigeodesics-in-planar-first-passage-percolation-September-24-2026/main.pdf): > Licea and Newman proved coalescence for each direction in a deterministic set of full Lebesgue measure and excluded bigeodesics whose two end-directions are prescribed in that set; see also. ## Other sources - [openai/math release notes (2026): model provenance and review status](https://github.com/openai/math/blob/main/README.md): “manuscripts and supporting proof artifacts produced by an internal OpenAI model” ## Related - [Exact three- and four-state reconstruction thresholds and four-state tree capacity](https://closedform.nishachay.tech/e/openai-math-2026-229/) - Probability and statistical mechanics - [The geometric phase diagram, diffusion, and spectra of random planar maps](https://closedform.nishachay.tech/e/openai-math-2026-211/) - Probability and statistical mechanics - [Critical percolation on every quasi-transitive graph](https://closedform.nishachay.tech/e/openai-math-2026-213/) - Probability and statistical mechanics - [The Benjamini–Schramm nonuniqueness conjecture](https://closedform.nishachay.tech/e/openai-math-2026-214/) - Probability and statistical mechanics - [Canonical O(3) continuum limit and exact O(4) mass asymptotics](https://closedform.nishachay.tech/e/openai-math-2026-215/) - Probability and statistical mechanics - [Probability and statistical mechanics](https://closedform.nishachay.tech/science/mathematics/probability-and-statistical-mechanics/) - Field · 29 results - [Open since the 1960s](https://closedform.nishachay.tech/open-since/1960s/) - Era · 33 results - [Lean-checked results](https://closedform.nishachay.tech/trust/lean-checked/) - Trust · 242 results - [Report an error](https://github.com/nishachay/closed-form/issues/new?template=report-error.yml&labels=entry-error&title=%5Bentry%20212%5D%20)