Symplectic ball packing in higher dimensions

1 paperLean

Resolves the Siegel–Yao conjecture for arbitrary capacities in every dimension \(2n\ge6\). Finitely many closed symplectic balls of capacities \(R_1,\ldots,R_k\) embed disjointly into an open ball of capacity R exactly when \(\sum_iR_i^n\lt R^n\) and \(R_i+R_j\lt R\) for every distinct pair i, j.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

Symplectic Ball Packings in Higher Dimensions

OpenAI · September 23, 2026

We prove that, for all integers n ≥ 3 and k ≥ 1 and all positive real capacities \(R_1,\ldots,R_k\), the closed standard symplectic \(2n\)-balls of these capacities embed disjointly into the interior of a ball of capacity R > 0 if and only if \(\displaystyle \sum_{i=1}^k R_i^n\lt R^n, \qquad R_i+R_j\lt R\quad(i\ne j).\) Capacity is π times the squared Euclidean radius, and each embedding is defined on a neighborhood of its closed source ball. This proves Siegel and Yao's Conjecture A.

Read PDF Download Source

Cite

@misc{OAI:Symplectic-Ball-Packings-in-Higher-Dimensions-September-23-2026,
  author = {{OpenAI}},
  title = {{Symplectic Ball Packings in Higher Dimensions}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Symplectic-Ball-Packings-in-Higher-Dimensions-September-23-2026/paper.pdf}{OAI:Symplectic-Ball-Packings-in-Higher-Dimensions-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):

Symplectic Ball Packings in Higher Dimensions

Scope

The formalization proves Siegel and Yao's ball-packing criterion in every symplectic dimension \(2n\) with \(n\ge3\). For \(k\ge1\) closed standard balls of positive capacities \(R_1,\ldots,R_k\), disjoint symplectic embeddings into the interior of a ball of capacity \(R\) exist exactly when \(\sum_i R_i^n<R^n\) and \(R_i+R_j<R\) for all \(i\ne j\). Capacity is \(\pi\) times squared Euclidean radius, and each embedding is defined on a neighborhood of its closed source ball. The linked statements include both the full equivalence and the necessity direction.

Comparator links

Result	Comparator statement
Exact criterion for higher-dimensional symplectic ball packings	BallPacking.lean
Necessity of the volume and pairwise capacity inequalities	BallPackingNecessity.lean

Scope note on GitHub →