Sharp Cartan–Hadamard isoperimetry and rigidity

Proves sharp Euclidean fillings in CAT(0) spaces and claims the generalized Cartan–Hadamard isoperimetric inequality.

2 papers September 23, 2026 Explained by AI

The isoperimetric inequality says a ball has the least boundary area for its volume. The Cartan–Hadamard conjecture says this stays true, or gets stronger, in spaces that curve like a saddle. One paper claims the conjecture in every dimension and for every curvature bound κ ≤ 0. It adds that only flat balls attain the flat bound. A second paper proves a sharp filling bound in CAT(0) spaces, which gives the flat case, and Lean checks it.

First step

1926

André Weil, whose work began the surface case of the comparison

Significance

Major

It settles a long-standing conjecture of comparison geometry in every dimension; the flat case has a Lean check.

Trust

Formal proof listed

Field

Differential geometry

2 papers

The explanation

Take a unit cube. Its volume is 1 and its surface area is 6. A round ball with volume 1 has radius about 0.620. Its surface area is about 4.836. In ordinary three-dimensional space, every shape of volume V has surface area at least 3 × (4π/3)^(1/3) × V^(2/3). For V = 1 that is the 4.836 of the ball, and the cube's 6 is larger. This is the isoperimetric inequality: among shapes of a given volume, the ball has the least boundary.

A Cartan–Hadamard manifold is a complete curved space with no holes to loop around and sectional curvature at most zero. Sectional curvature at most zero means it curves like a saddle or is flat in every direction. Suppose the curvature is at most some κ ≤ 0. The generalized Cartan–Hadamard conjecture says every region then has at least the boundary area of the equal-volume ball in constant curvature κSource 1. Comparing balls alone does not settle it, because arbitrary regions must be handled. Weil started the surface case in 1926Source 2. Kleiner proved dimension threeSource 3, and Croke proved the flat comparison in dimension fourSource 4. A recent preprint reached the flat comparison in dimensions three through nineSource 5.

The first paper claims the conjecture in every dimension, for every κ ≤ 0Source 6. It covers every set of finite volume and finite perimeter, not only smooth regions. It also claims a rigidity result. If a bounded region meets the flat bound exactly, the region itself is a round flat ball. The space outside it need not be flatSource 7.

The second paper works in CAT(0) spaces. These are spaces where every triangle is at least as thin as a flat triangle with the same side lengths. It takes a closed n-dimensional cycle, a generalised surface that may have overlapping layers. It proves the cycle bounds a filling of mass at most c_n times the cycle's mass to the power (n + 1)/nSource 8. For n = 2, c_2 = 1/(6√π), about 0.0940Source 9. A unit sphere has area 4π, about 12.566. Then c_2 × (4π)^1.5 works out to exactly 4π/3, about 4.189, the volume of the unit ball. So round spheres show the constant cannot be improved. As a corollary, the flat Cartan–Hadamard inequality holds in every dimension from three upSource 10.

How sure is this? Lean, a computer proof checker, has formal statements of the filling result and of the optimality of its constant. So the second paper proves these, as far as the Lean statements match the paper. Lean does not cover the first paper's curved comparison for κ < 0 or its rigidity result; those are claims. No specialist review is published.

What it doesn't show. This does not cover spaces with some positive curvature, where the flat isoperimetric inequality can fail.

Where it came from

This result comes from an unreleased OpenAI model, published in the openai/math release on 6 October 2026.

Hype check

Major. The flat case has a Lean-checked route through the filling paper. The curved case κ < 0 and the rigidity result rest on the first paper alone, without Lean or published specialist review.

Words used

Isoperimetric inequality: A lower bound on boundary area in terms of enclosed volume, with balls as the best case.
Sectional curvature: The curvature of a space along each two-dimensional direction; negative means saddle-like.
Cartan–Hadamard manifold: A complete, simply connected curved space whose sectional curvature is never positive.
CAT(0) space: A space where every triangle is at least as thin as the flat triangle with the same side lengths.
Integral cycle: A generalised closed surface with whole-number layers, allowed to be singular.
Filling: A higher-dimensional piece whose boundary is a given cycle.
Mass: The total size of a cycle or filling, counting layers.

The original papers (2)

Lean notes

All quoted lines (10)

The generalized Cartan–Hadamard isoperimetric conjecture asserts that if its sectional curvature is at most $\kappa\le0$ , then every relatively compact smooth domain has boundary area at least that of the equal-volume ball in the simply connected space form of curvature $\kappa$ .
Generalized Cartan–Hadamard isoperimetry and Euclidean equality rigidity Back to text
The surface inequality originates in Weil's work and the subharmonic-function approach of Beckenbach and Rad\'o; Bol developed the comparison with nonzero model curvature.
Generalized Cartan–Hadamard isoperimetry and Euclidean equality rigidity Back to text
We use the smooth surface formulation of Chavel and Feldman. Kleiner proved the model comparison in dimension three, including its equality case.
Generalized Cartan–Hadamard isoperimetry and Euclidean equality rigidity Back to text
Kleiner proved the model comparison in dimension three, including its equality case. Croke proved the sharp Euclidean comparison in dimension four.
Generalized Cartan–Hadamard isoperimetry and Euclidean equality rigidity Back to text
Chen, Ghomi and Wang establish Euclidean comparison and rigidity in dimensions three through nine, report calibration verification through at least dimension thirteen, and announce generalized comparison in dimensions four and five.
Generalized Cartan–Hadamard isoperimetry and Euclidean equality rigidity Back to text
We resolve the generalized Cartan–Hadamard isoperimetric conjecture in every dimension.
Generalized Cartan–Hadamard isoperimetry and Euclidean equality rigidity Back to text
It does not require the ambient manifold outside that region to be flat.
Generalized Cartan–Hadamard isoperimetry and Euclidean equality rigidity Back to text
holds in every proper CAT(0) space, in all cycle dimensions at least two.
Sharp integral fillings in CAT(0) spaces Back to text
c_2=\frac16\sqrt\pi,
Sharp integral fillings in CAT(0) spaces Back to text
following positive answer in dimensions at least three.
Sharp integral fillings in CAT(0) spaces Back to text

Other sources

OpenAI, “Sharp integral fillings in CAT(0) spaces”
openai/math, Lean scope note for family 337 The formalization proves the sharp Euclidean filling inequality for every compactly supported integral $n$ -cycle in a proper $\mathrm{CAT}(0)$ space, for $n\ge2$ .
openai/math release notes (2026): model provenance and review status manuscripts and supporting proof artifacts produced by an internal OpenAI model

336Spectral scalar curvature, Urysohn width, and macroscopic dimensionDifferential geometry
338Yau's uniformization conjectureDifferential geometry
335Gromov’s integral scalar-curvature bound for simplicial volumeDifferential geometry
339Katok's entropy rigidity conjectureDifferential geometry
333Smooth isometric immersions of surfaces into ℝ 4Differential geometry

Browse Differential geometry Curvature and geometric flows Open since before 1940 Lean-checked results