A random straight line?
Two preprints claim that random grids almost surely contain no bigeodesics, and that the exponential limit shape has no corners and no flat sides
Covers result 212 in OpenAI’s catalog: all 2 papers. See its connections to other results and the work it cites.
4:53. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
Give every edge of the square grid an independent random travel time with the same law. The passage time between two points is the cost of the cheapest route, a geodesic. In our 4 × 4 example the cheapest way across costs 2.55, along a staircase; the obvious route along the edges costs 5.15. Hammersley and Welsh introduced this model in 1965, and a classical shape theorem says that, under a mild moment condition, the set reachable by time t grows like a fixed convex shape.
Two old questions. As Kesten tells it, Furstenberg asked whether there is a bigeodesic, a kind of random straight line: an infinite path running off in both directions, every piece of which is a cheapest route. With every edge costing 1, every row is one; a planted highway makes one too. And could the limit shape have a corner or a flat side?
Result 212 bundles two OpenAI preprints dated September 24, 2026. The first (39 pages) claims that with probability one there are no bigeodesics at all, all directions at once, for any edge law with no atoms where the cheapest of four edges has a finite second moment; single edges may even have infinite average cost, and nothing is assumed about the limit shape. The second (95 pages) claims that for exponential weights the limit shape is strictly convex, with no flat sides, and has a C¹ boundary with no corners; for every Gamma law, it claims the boundary has no corners.
What it doesn’t claim
Other dimensions; laws with atoms, where ties appear; the conjecture without the moment condition; strict convexity beyond exponential weights; any formula for the shape. The time constant of about 0.42 along an axis is our simulation, still drifting at distance 350, not the paper’s.
Where it stands
- Posted as preprints
- OpenAI, two papers (39 and 95 pages), dated September 24, 2026
- Peer reviewed
- Not yet
- Checked in Lean
- Only the no-corners half of the shape paper (docs)
Last checked October 19, 2026. Neither preprint has been revised since they were added to the repository in its initial commit on October 6, 2026. Only the no-corners half of the shape paper is formalized in Lean, for exponential and every Gamma law (the checked Gamma statement): about 37,000 lines with no unproved steps; we did not build it. The no-flat-sides argument and the no-bigeodesics paper are not formalized. Neither paper is among those OSVerify reviewed, and we found no expert reaction.
How the proof goes
- Labels. Every infinite geodesic carries a label, the slope of its Busemann function. Geodesics with the same fixed label merge, and for any one fixed label, almost surely no bigeodesic uses it. The difficulty is that a bigeodesic could pick an exceptional label that depends on the environment, and there are uncountably many labels to rule out.
- A tax. Raise random edge costs at height h with probability shrinking like 1/(h log h). The world looks statistically almost the same, yet every marked bigeodesic pays a toll that grows without bound. A conservation law for Busemann functions along a line caps the total toll: too many tolls, too small a budget.
- The shape. A corner would penalize every sideways step; counting rare cheap pieces with the van den Berg–Kesten inequality shows every long path would then cost more than the shape allows. A flat side would mean the best road along it can be improved by a fixed factor at every scale, forever, which is impossible; that part runs about 60 pages.
As an illustration only, in our simulation the chance that a geodesic passes through its midpoint falls from 0.77 to 0.10 as the distance grows. Simulations cannot see a bigeodesic, or a flat side.
The numbers in the video
- Worked patch (ours): cheapest route 2.55, unique among 184 simple paths; along the edges 5.15. With constant weights, 12,870 cheapest routes across an 8 × 8 square.
- Exponential simulation (ours): time constant about 0.42 along an axis at distance 350, still drifting; diagonal over axis about 1.013; 3,040 geodesics from the origin share a few dozen trunks; midpoint frequencies 0.77 down to 0.10. Sums of the raise probabilities (with the paper’s small constant set to 1): 2.3 at 10², 3.7 at 10⁸. The Lean line count is ours.
Read the source
- No bigeodesics in planar first-passage percolation (PDF), 39 pages.
- Strict convexity and differentiability of the planar exponential first-passage limit shape (PDF), 95 pages.
- The Lean formalization notes.
- The collection’s catalog, where this is result 212.
The 2 papers in this result
OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.
Transcript
Read the full script
0:00The question
Give every edge of the square grid a random travel time, independent and with the same law. The passage time between two points is the cost of the cheapest route, and that route is a geodesic. In this small patch, the cheapest way across costs 2.55, along a staircase; the obvious route along the edges costs 5.15. Our computer checked all 184 simple paths. Now let the grid run to infinity. Hammersley and Welsh introduced this model in 1965. The set of points you can reach by time t grows, and a classical shape theorem says that, under a mild moment condition, it grows like a fixed convex shape, the limit shape. Two old questions. First, as Kesten tells it, Furstenberg asked whether there is a bigeodesic, a kind of random straight line: an infinite path running off in both directions, every piece of which is a cheapest route. With every edge costing one, every row is one, and there are 12,870 cheapest routes across an 8 × 8 square. A planted highway of cheap edges makes one too. Do random weights ever build one? Second, could the limit shape have a corner or a flat side? For exponential weights, our simulation puts it within about 1.5% of a circle, far too coarse to see either.
1:23The claim
Result 212 bundles two OpenAI preprints, both dated September 24, 2026. The first, 39 pages, claims that with probability one there are no bigeodesics at all, all directions at once, for any edge law with no atoms where the cheapest of four edges has a finite second moment. Single edges may even have infinite average cost. It assumes nothing about the limit shape. The second, 95 pages, claims that for exponential weights the limit shape is strictly convex, with no flat sides, and has a boundary with no corners; for every Gamma law, it claims the boundary has no corners. Not claimed: other dimensions; laws with atoms, where ties appear; the conjecture without the moment condition; strict convexity beyond exponential weights; or any formula for the shape. The time constant of about 0.42 along an axis is our simulation, still drifting at distance 350, not the paper’s.
2:27How the proof goes
Every infinite geodesic carries a label, the slope of its Busemann function, which measures how far ahead each point is on the way to infinity. Geodesics with the same fixed label merge, and our simulation shows something similar: 3,040 geodesics from the origin share a few dozen trunks. For any one fixed label, almost surely no bigeodesic uses it. The difficulty is that a bigeodesic could pick an exceptional label that depends on the environment, and there are uncountably many labels to rule out. The paper’s answer is a tax. Raise random edge costs at height h with probability shrinking like one over h log h. The world looks statistically almost the same, yet every marked bigeodesic pays a toll that grows without bound, like log log of the distance: our sums, without the paper’s small constant, reach only 3.7 by a hundred million. A conservation law for Busemann functions along a line caps the total toll. Too many tolls, too small a budget: contradiction. The shape paper works in two parts. A corner would penalize every sideways step; a count of rare cheap pieces, with the van den Berg–Kesten inequality, shows every long path would then cost more than the shape allows. A flat side would mean the best road along it can be improved by a fixed factor at every scale, forever, which is impossible; that part runs about 60 pages. As an illustration only, the chance that a geodesic passes through its midpoint falls from 0.77 to 0.1 as the distance grows; simulations cannot see a bigeodesic, or a flat side.
4:12Where it stands
Both preprints are unrefereed and have not been revised. Only the no-corners half is formalized in Lean, for exponential and every Gamma law: about 37,000 lines, with no unproved steps, and the statements pinned down exactly; we did not build it. The no-flat-sides argument and the no-bigeodesics paper are not formalized. Neither paper is among those OSVerify reviewed, and we found no expert reaction. If they hold, a random grid almost surely never builds an infinite straight road, and the shape every exponential ball grows into has no corners and no flat sides.
Spot a mistake?
This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.