The ball wins everywhere?

The claim, in plain words

On a flat plane, among all regions of a given area, the round disk has the shortest boundary. The Cartan–Hadamard conjecture says the same bound holds in every complete, simply connected space whose curvature is nowhere positive: curving like a saddle can only make boundaries longer, never shorter. Our computer checks this on a saddle surface, where boundary squared over 4π times area grows from about 1.06 to 2.7, while on a sphere, which curves the other way, it drops below 1. The generalized version asks for more: if the curvature is at most some negative number, every region should have at least the boundary of the equal-volume round ball in the curved model space.

The conjecture is usually credited to Aubin in the mid-1970s, and to Gromov and to Burago and Zalgaller. Weil proved the flat case for surfaces in 1926, and Bol the curved case in 1941. Croke did the flat case in dimension 4 in 1984, and Kleiner dimension 3, curved case included, in 1992. A claimed proof in all dimensions by Ghomi and Spruck in 2019 ran into a gap, and its published version proves only a conditional result. In September 2026, days before the release papers’ date, Chen, Ghomi and Wang posted a proof of the flat case in dimensions 3 through 9.

Result 337 is two OpenAI papers, both dated September 23 and made public October 6, 2026. The first, 42 pages, claims the generalized inequality in every dimension: any region of finite volume has at least the boundary of the equal-volume ball in the model space. Its own argument covers dimension 4 and up; dimensions 2 and 3 are quoted from Weil, Bol and Kleiner. It also claims that a bounded region with exactly the flat bound must be, inside, a perfectly flat round ball. The second, 46 pages, works in spaces of nonpositive curvature that may be singular: every closed surface of dimension 2 or more, counted with integer multiplicity, bounds a filling no larger than the round ball allows, with the best possible constant. That gives the flat inequality again in dimensions 3 and up.

What it doesn’t claim

Not claimed: that the whole space must be flat when equality holds; an equality statement for negative curvature; or Gromov’s stronger filling conjecture for such spaces, which also prescribes the shape of the filling.

Where it stands

Posted as preprints

OpenAI, 2 papers (42 and 46 pages), dated September 23, 2026

Peer reviewed

Not yet

Formalized in Lean

The second paper’s filling theorem and its constant; not the first paper (docs)

Last checked October 19, 2026. Both papers are unrefereed and unchanged since release. Lean covers only the second paper: its main filling theorem and the optimality of the constant, in about 440 files and 66,000 lines, not run by us, though much of the optimality part repeats the main part. The step from fillings to regions in a manifold, and the whole first paper, are not formalized. Three outside projects re-ran the check and it passed, two of them also with a second kernel. We found no specialist assessment and no reported error. OSVerify has not reviewed it.

How the proof goes

1. Paper 1: a map to the sphere. The first paper maps the space into a round sphere with a stereographic map adapted to the curvature, and balances it so the image is centered. In dimension 4 and up, that gives a sharp Sobolev inequality on every hypersurface; our computer checks that round spheres give equality and stretched capsules do not. Testing it with a constant function turns into a differential inequality for the least boundary area inside a large ball, a setup credited to Kleiner, and integrating it gives exactly the model bound; our computer confirms that its equality case traces the model profile to 12 digits.
2. Paper 2: chords that cannot be both short and long. The second paper takes an extremal cycle that would beat the bound. In dimension 2 a radial first-variation argument rules it out. Above 2, an almost sharp Sobolev inequality produces a function whose weighted chords have mean square below 2, while curvature comparison forces at least 2. Round spheres attain the constant: for two-dimensional spheres it is 1 over 6√π.

The numbers in the video

• Ours: on a saddle surface, boundary squared over 4π times area is 1.06, 1.21, 1.66 and 2.73 for growing disks; on sphere caps it falls to 0.98, 0.77, 0.29 and 0.005.
• Ours: the equality case of the first paper’s profile inequality traces the model profile to about 12 digits.
• Ours: the filling constant for two-dimensional cycles is 1/(6√π) ≈ 0.0940, attained exactly by round spheres.
• Lean: 442 files and 65,872 lines in the import closure of the two comparators, 330 files and 50,219 lines for the main theorem alone (counted by us; not run by us).

Read the source

• Generalized Cartan–Hadamard isoperimetry and Euclidean equality rigidity (PDF), 42 pages.
• Sharp integral fillings in CAT(0) spaces (PDF), 46 pages.
• The Lean formalization notes.
• The collection’s catalog, where this is result 337.

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.

• Generalized Cartan–Hadamard isoperimetry and Euclidean equality rigidity main paper
• Sharp integral fillings in CAT(0) spaces companion

Transcript

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.