Fat triangles from a tensor?

The claim, in plain words

On a sphere, triangles are fatter than flat ones. Our computer finds that a triangle whose sides are quarter circles has angles adding to 270 degrees, against 180 in the plane and about 133 in the hyperbolic plane. Alexandrov turned this into a definition that needs only distances: a space has curvature at least κ if small triangles are at least as fat as in the model surface of curvature κ. A paper cone passes when its rim is at most 2π long; our random four-point tests find no failures there, and thousands once the rim is longer.

A second theory, built on optimal transport, captures lower bounds on Ricci curvature, an average of curvatures, through RCD spaces, which carry a calculus of gradients and Hessians. In 2019, Nicola Gigli used that calculus to define a curvature tensor by integration, and conjectured that a lower bound on it is exactly Alexandrov’s condition, for spaces measured by their own volume. Alexandrov spaces were known to be RCD spaces, by work of Petrunin and of Zhang and Zhu. In 2023, Brena and Gigli still called the meaning of the tensor bound unknown.

Result 356 is two OpenAI papers, dated September 24 and made public October 6, 2026. The main paper, 53 pages, claims Gigli’s conjecture in every dimension two and up: a space is an n-dimensional Alexandrov space with curvature at least κ exactly when, measured by n-dimensional volume, it is an RCD space with Ricci bound (n − 1)κ and full support, and Gigli’s sectional curvature is at least κ for all his test fields. The 11-page companion proves a tool: a weak Hessian bound holds along every shortest path, not just almost every one.

What it doesn’t claim

Not claimed: dimension one, other measures, or upper curvature bounds. For surfaces, the direction from the Ricci condition to fat triangles was already proved by Lytchak and Stadler in 2018, a result the paper does not cite. We found no competing claim.

Where it stands

Posted as a preprint

OpenAI, 53 + 11 pages, dated September 24, 2026

Peer reviewed

Not yet

Formalized in Lean

The companion lemma only, not the characterization (scope notes)

Last checked October 19, 2026. Both papers are unrefereed and unchanged since release. The Lean formalization covers only the companion’s theorem, about 65,000 lines, not run by us, and it follows a different route from the companion’s own proof. The characterization itself has no formal proof. An AI audit found no gap, but did not check the cited theorems or the companion. We found no specialist comment and no reported error. OSVerify has not reviewed it.

How the proof goes

1. Triangles to tensor, and back. The forward direction starts from triangles. The paper moves mass a short way along pairs of gradient directions and compares how far it travels with how far apart the two endpoints land. At almost every point the space looks Euclidean up close, and expanding the model triangle to fourth order produces κ/6, matching one sixth of the tensor term, so the tensor bound follows. The converse runs a smoothed version of the second-variation formula along shortest paths, using heat flow, and builds frames of test gradients at every time along almost every path. That gives a Hessian comparison for the squared distance.
2. Every shortest path. The companion upgrades that bound from almost every shortest path to every one. It reweights the measure, which shifts the Ricci bound by the Hessian bound, and concentrates mass from two shrinking balls onto a single geodesic, while the weight grows. Brena and Gigli had suggested this change of measure and named the missing regularity step; the companion supplies it. Along every short geodesic, a function of the distance to a fixed point then obeys the model equation as an inequality, which our computer checks holds exactly in the three model planes. That gives triangle comparison, and the globalization theorem for Alexandrov spaces finishes.

The numbers in the video

• Ours: a triangle with sides of length π/2 has angles summing to 270° on the unit sphere, 180° in the plane and about 133° in the hyperbolic plane.
• Ours: on paper cones, the four-point test fails in 0 of 20,000 random samples when the rim is at most 2π, and in 3,090 and 5,132 at 2.2π and 3π.
• Ours: the model equation y″ + κℓ²y = ℓ² holds exactly along geodesics in the three model planes.
• Lean: 542 files and 65,542 lines in the import closure of the companion's comparator (counted by us; not run by us).

Read the source

• Gigli’s distributional curvature characterization of Alexandrov spaces (PDF), 53 pages.
• Weak Hessian bounds along every geodesic in RCD spaces (PDF), 11 pages.
• The Lean formalization notes.
• The collection’s catalog, where this is result 356.

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.

• Gigli’s distributional curvature characterization of Alexandrov spaces main paper
• Weak Hessian bounds along every geodesic in RCD 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.