Planar first-passage geometry and the absence of bigeodesics

Proves that planar first-passage percolation has no doubly infinite geodesic for iid nonnegative nonatomic edge weights when the minimum of four weights has finite second moment. For exponential weights, the limit shape is strictly convex with C¹ boundary. Differentiability also holds for every Gamma law with positive shape and rate. (Lean)

Manuscripts (2)

No bigeodesics in planar first-passage percolation

September 24, 2026 · source · cite as \cite{OAI:No-bigeodesics-in-planar-first-passage-percolation-September-24-2026}

We prove that planar first-passage percolation with independent identically distributed nonnegative nonatomic edge weights has almost surely no doubly infinite geodesic, provided the minimum of four independent weights has finite second moment. This resolves the planar no-bigeodesics conjecture under that moment assumption. The conclusion rules out all bigeodesics simultaneously, without any regularity assumption on the limit shape.

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

September 24, 2026 · source · Lean formalization available · cite as \cite{OAI:Strict-convexity-and-differentiability-of-the-planar-exponential-first-passage-limit-shape-September-24-2026}

We prove that the limit shape of undirected nearest-neighbor first-passage percolation on ℤ² with independent exponential edge weights is strictly convex and has a C¹ 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.

Result 212 · Probability and statistical mechanics. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.