∑math20

Probability and statistical mechanics · Result 212

Planar first-passage geometry and the absence of bigeodesics

2 papersLean

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 C1 boundary. Differentiability also holds for every Gamma law with positive shape and rate.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 2

First page of No bigeodesics in planar first-passage percolation

No bigeodesics in planar first-passage percolation

OpenAI · 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.

Read PDF Download Source

Cite
@misc{OAI:No-bigeodesics-in-planar-first-passage-percolation-September-24-2026,
  author = {{OpenAI}},
  title = {{No bigeodesics in planar first-passage percolation}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/No-bigeodesics-in-planar-first-passage-percolation-September-24-2026/main.pdf}{OAI:No-bigeodesics-in-planar-first-passage-percolation-September-24-2026}},
  year = {2026}
}
First page of Strict convexity and differentiability of the planar exponential first-passage limit shape

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

OpenAI · September 24, 2026

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

Read PDF Download Source

Cite
@misc{OAI:Strict-convexity-and-differentiability-of-the-planar-exponential-first-passage-limit-shape-September-24-2026,
  author = {{OpenAI}},
  title = {{Strict convexity and differentiability of the planar exponential first-passage limit shape}},
  howpublished = {OpenAI Math Release preprint
                  \href{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}{OAI:Strict-convexity-and-differentiability-of-the-planar-exponential-first-passage-limit-shape-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalization proves differentiability of the planar first-passage time-constant norm for independent Gamma edge weights of every positive shape and rate. The norm is differentiable away from the origin, and its unit sphere has a \(C^1\) boundary. This includes the exponential model, for which the linked statement also gives a unique supporting line at every boundary point.

The paper also claims strict convexity for the exponential limit shape. Strict convexity is outside these selected differentiability statements.

Comparator links

ResultComparator statement
Differentiability of the exponential first-passage limit shapePlanarFirstPassage.lean
Differentiability for every positive Gamma edge-weight lawGammaPassage.lean

Scope note on GitHub →