∑math20

Differential geometry · Result 354

The isoperimetric profile of the cubic three-torus

1 paperLean

Determines the isoperimetric profile of the unit cubic flat three-torus and classifies every finite-perimeter minimizer: balls, circular tubes around shortest closed geodesics, coordinate slabs, and their complements. The transition volumes are \(4\pi/81\) and \(1/\pi\), with exactly the adjacent two types minimizing at each transition.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of The Isoperimetric Conjecture for the Cubic Flat Three-Torus

The Isoperimetric Conjecture for the Cubic Flat Three-Torus

OpenAI · September 24, 2026

We prove the isoperimetric conjecture for the cubic flat three-torus and classify all minimizers, including the equality cases at the transition volumes \(4\pi/81\) and \(1/\pi\). The minimizing regions are balls, circular tubes about shortest closed geodesics, coordinate slabs, and their complements.

Read PDF Download Source

Cite
@misc{OAI:The-Isoperimetric-Conjecture-for-the-Cubic-Flat-Three-Torus-September-24-2026,
  author = {{OpenAI}},
  title = {{The Isoperimetric Conjecture for the Cubic Flat Three-Torus}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-Isoperimetric-Conjecture-for-the-Cubic-Flat-Three-Torus-September-24-2026/article.pdf}{OAI:The-Isoperimetric-Conjecture-for-the-Cubic-Flat-Three-Torus-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

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

Scope

The formalization determines the isoperimetric profile and all minimizers in the unit cubic flat three-torus. At every volume \(0<V<1\), a minimizer exists, and the minimizers, up to null-set changes, are exactly balls, circular tubes about shortest closed geodesics, coordinate slabs, and their complements in the appropriate volume ranges.

The classification includes all equality cases at the transition volumes \(4\pi/81\) and \(1/\pi\), and every minimizer has the stated candidate-profile perimeter.

Comparator links

ResultComparator statement
Isoperimetric profile and all minimizers in the cubic flat three-torusCubicTorus.lean

Scope note on GitHub →