Sharp Cartan–Hadamard isoperimetry and rigidity

2 papersLean

Proves generalized Cartan–Hadamard isoperimetry in every dimension: in a complete simply connected manifold with sectional curvature at most κ ≤ 0, every finite-volume finite-perimeter set satisfies the sharp comparison with the equal-volume model ball. Bounded positive-volume equality regions for κ = 0 are Euclidean balls. Also proves sharp Euclidean filling bounds for compactly supported integral n-cycles, n ≥ 2, in arbitrary proper CAT\((0)\) spaces.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 2

Generalized Cartan–Hadamard isoperimetry and Euclidean equality rigidity

OpenAI · September 23, 2026

We resolve the generalized Cartan–Hadamard isoperimetric conjecture in every dimension. In a complete simply connected smooth manifold with sectional curvature at most κ ≤ 0, every finite-volume set of finite ambient perimeter has perimeter at least that of the equal-volume ball in curvature κ. For bounded positive-volume sets, equality in the Euclidean comparison holds precisely when the set agrees up to null sets with an open region isometric, with its induced metric, to a round Euclidean ball.

Read PDF Download Source

Cite

@misc{OAI:Generalized-Cartan-Hadamard-isoperimetry-and-Euclidean-equality-rigidity-September-23-2026,
  author = {{OpenAI}},
  title = {{Generalized Cartan--Hadamard isoperimetry and Euclidean equality rigidity}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Generalized-Cartan-Hadamard-isoperimetry-and-Euclidean-equality-rigidity-September-23-2026/paper.pdf}{OAI:Generalized-Cartan-Hadamard-isoperimetry-and-Euclidean-equality-rigidity-September-23-2026}},
  year = {2026}
}

Sharp integral fillings in CAT(0) spaces

OpenAI · September 23, 2026

Every compactly supported integral n-cycle, n ≥ 2, in a proper CAT(0) space bounds a compactly supported integral current with the sharp Euclidean mass bound. The theorem allows arbitrary integer multiplicities and unrestricted ambient dimension. In particular, we prove the Euclidean Cartan–Hadamard isoperimetric conjecture in dimensions at least three.

Read PDF Download Source

Cite

@misc{OAI:Sharp-integral-fillings-in-CAT(0)-spaces-September-23-2026,
  author = {{OpenAI}},
  title = {{Sharp integral fillings in CAT(0) spaces}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Sharp-integral-fillings-in-CAT\%280\%29-spaces-September-23-2026/paper.pdf}{OAI:Sharp-integral-fillings-in-CAT(0)-spaces-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

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

Sharp integral fillings in \(\mathrm{CAT}(0)\) spaces

Scope

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\). It constructs a compactly supported integral filling whose mass is at most \(C_n\) times the boundary mass to the power \((n+1)/n\), where \(C_n\) is the Euclidean isoperimetric coefficient. Integer multiplicities and the ambient dimension are unrestricted.

A second statement proves that this coefficient is optimal by giving, in Euclidean space, a cycle for which every compactly supported integral filling has at least that mass. This yields the selected integral-current form of the Cartan–Hadamard isoperimetric conjecture.

Comparator links

Result	Comparator statement
Optimality of the Euclidean filling coefficient	FillingCoefficient.lean
Sharp integral fillings in proper \(\mathrm{CAT}(0)\) spaces	SharpCAT0Filling.lean

Scope note on GitHub →