Symplectic Ball Packing: How OpenAI Proved Exactly Which Balls Fit

Two balls in six dimensions can use just 43.2% of a target ball’s volume and still be impossible to pack inside it. Take two balls of capacity 0.6 and a target of capacity 1. Their capacities add to 1.2, which violates Gromov’s two-ball bound. OpenAI’s September 23, 2026 preprint proves that for symplectic ball packing in real dimension six or higher, this pairwise bound and the total-volume bound are the complete test. If both inequalities are strict, even a collection of unequal closed balls admits disjoint symplectic embeddings into the open target. The proof finds those embeddings by turning surplus volume into usable area over a surface with a handle.

1. Symplectic Ball Packing: When Can Several Balls Fit Inside One?

A symplectic packing places the images of finitely many balls inside one target with no intersections, even along the source boundaries. The maps can bend and stretch each ball while preserving the symplectic form.

The preprint Symplectic Ball Packings in Higher Dimensions states the result as Theorem 1.1. Earlier work gave both obstructions. The new part is sufficiency. Once the requested balls pass both tests, the proof constructs a packing through auxiliary geometric models.

2. Symplectic Capacity, Embeddings, and the Geometry of Phase Space

Write each complex coordinate as $z_j=x_j+\mathrm{i}y_j$. The standard symplectic form pairs the real coordinates $x_j$ and $y_j$, as position and momentum are paired in phase space. With $n$ such pairs, the real dimension is $2n$. The closed ball and the standard form are

The capacity parameter is $R=\pi r^2$ for Euclidean radius $r$. One way to read this normalization is that a central disk in one complex coordinate plane has area $R$. An embedding $f$ satisfies $f^*\omega_0=\omega_0$, so the form evaluated on two tangent vectors agrees with its evaluation on their images under the derivative. The derivative may stretch one coordinate and contract its conjugate coordinate by the reciprocal factor. That preserves the two-form while changing lengths.

Taking the $n$th exterior power of the form and dividing by $n!$ gives the symplectic volume element. Integrating it over the ball gives $R^n/n!$. Doubling the Euclidean radius multiplies capacity by four and the volume in six dimensions by 64.

3. Why Volume Alone Cannot Solve Symplectic Ball Packing

Because the images of the closed balls are compact and lie inside the open target, they all fit in a smaller concentric ball of capacity $\sigma<R$. Disjointness and volume preservation give $\sum_i R_i^n\leq\sigma^n$. The same smaller target lets the Gromov two-ball theorem impose $R_i+R_j\leq\sigma$ for each pair. The compactness argument makes both resulting bounds strict relative to $R$.

The two-ball obstruction comes from Gromov’s pseudoholomorphic-curve theory. When a suitable curve is forced through the centers of both embedded balls, its symplectic area has to accommodate the contributions from both balls. A capacity sum captures that restriction even when the occupied fraction of the ambient volume is small.

Here normalized volume means the sum of cubed capacities divided by the cube of the target capacity. The factors of $1/3!$ cancel. For the first pair in the table, 56.8% of the target volume would remain unused. That surplus cannot compensate for the pairwise capacity violation.

4. OpenAI’s Exact Packing Theorem: Two Inequalities, No Further Obstructions

Let $n\geq3$ and $k\geq1$ be integers, and let $R,R_1,\ldots,R_k$ be positive real capacities. Theorem 1.1 says that the $k$ closed standard balls of capacities $R_1,\ldots,R_k$ embed disjointly into the interior of the standard target ball of capacity $R$ if and only if

Each symplectic embedding is defined on an open neighborhood of its closed source ball. Equality in either test rules out the packing with these source and target conventions. With one source there is no pair to check, and the volume test reduces to $R_1<R$. In that case ordinary inclusion gives the embedding.

For eight equal balls of capacity 0.49 in a six-dimensional unit target, the pairwise sum is 0.98 and the normalized volume is $8(0.49)^3=0.941192$. The theorem guarantees a packing. Raising the capacity of each one to 0.5 makes the pairwise sum and total normalized volume both exactly 1, so the closed balls cannot fit into the open target. A family of packings can approach full volume as the common capacity approaches 0.5 from below.

5. The Siegel–Yao Conjecture and the Limits of Earlier Packing Results

Kyler Siegel and Yuan Yao proposed precisely this criterion as Conjecture A. Earlier packing-stability theorems identified regimes where volume controls existence. Biran established equal-ball stability for closed symplectic four-manifolds with rational symplectic class. Buse and Hind extended equal-ball stability to higher-dimensional balls and projective spaces. Strong packing stability for closed symplectic four-manifolds extends the idea to unequal balls whose capacities are all sufficiently small.

Stability leaves open what happens for a finite list with a possible large ball. In real dimension four, additional obstructions from pseudoholomorphic curves are essential. Five equal balls of capacity 0.42 pass both tests in a four-dimensional unit target, with pair sum 0.84 and normalized volume 0.882. The known five-ball volume fraction is at most $20/25=0.8$, which rules out that packing. Siegel and Yao also studied products of four-dimensional balls with a fixed closed symplectic surface, where the four-dimensional packing obstructions persist. The standard higher-dimensional balls in Theorem 1.1 have a different geometry from those product targets.

6. The Proof’s Central Idea: Turning Unused Volume Into an Area Profile

The proof normalizes the target capacity to one by applying the same dilation to source and target. It works over a punctured surface with a handle, with a toric fiber in $\mathbb{C}^m$, where $m=n-1$. The moment coordinates $p_j=\pi|z_j|^2$ record the area parameter in each complex coordinate. The allowed moments form a downward polytope $\Delta$. Decreasing any coordinate while keeping it nonnegative stays inside the domain.

At fixed moment $p$, let $H(p)$ be the limiting total area of the surface. An auxiliary ball of capacity $r_i$, chosen slightly larger than the requested one, needs the area left after accounting for the fiber moments. Writing $x_+=\max(x,0)$, the unused-area profile is

The positive-part expression comes from slicing a standard ball along all but its last complex coordinate. The remaining disk has area $r_i-\sum_j p_j$ when that difference is positive. The integral of this requirement over the moment simplex is the auxiliary ball’s volume. In the models used in the proof, the integral of $H$ can be made close enough to the available volume that the integral of $P$ is positive. Some moments can still have a local shortage.

7. Hamiltonian Comparison: How Rearrangement Creates Room

Lemma 2.1 assumes that $P$ is continuous and concave, has positive mean, and stays uniformly positive outside a smaller radial copy of $\Delta$. In each geometric model, sufficiently near the outer faces, every ball’s area demand has already dropped to zero, while the truncated model still has positive base area.

Lemma 2.2 sorts the values of a convex function along one moment coordinate at a time. On each slice, increasing rearrangement keeps the distribution of function values, hence the integral. It also preserves convexity, and the composition $\mathcal{R}$ through all coordinates preserves earlier monotonicity. Applying it to $\lambda F-P$ gives a contraction in the uniform norm for $0<\lambda<1$. Its fixed point has negative mean because $P$ has positive mean. For $\lambda$ close enough to one, convexity and positivity near the outer faces turn that mean estimate into a uniform comparison gap.

Lemma 2.3 realizes the coordinate rearrangements up to arbitrarily small one-sided errors using smoothly varying planar disk maps lifted to Hamiltonian maps of the fiber. Those errors and the smoothing of the fixed point fit inside the gap. The resulting smooth toric function $K$ and Hamiltonian diffeomorphism $q$ obey

Here $u$ is a point of the fiber and both functions are read through its moment coordinates. The generating Hamiltonians commute with each defining outer-face moment in a collar of that face. Keeping these levels invariant lets the next stage use the rearrangement without moving the boundary of the model.

8. The Handle Construction: From Area Inequalities to Disjoint Ball Layers

Lemma 3.3 turns the uniform gap into a packing over a compact bordered piece of the surface. The integrated area profiles converge uniformly to $H$, so a finite piece retains enough of the gap. Concavity is required for the limiting unused-area profile.

Inside the handle, the proof takes two annuli around essential circles that intersect once. A closed one-form supported in the transverse annulus integrates to one around the core circle of the first. Its nonzero period supplies a coordinate on a strip of that annulus. The proof concentrates most of the surface area there and inserts the fiber isotopy by letting its Hamiltonian time vary across the strip.

The interpolating symplectic forms differ by exact forms. The coefficient of the closed one-form grows in successive, disjoint layers, each allotted an area profile strictly greater than the corresponding ball needs. In each layer, a change of coordinates makes the form a product and provides room for the ball with its original requested capacity. A relative Moser isotopy carries the packing back to the initial form while preserving the outer faces and fixing a collar of the surface boundary.

9. Three Geometric Cases That Complete the Packing Proof

For a unit target, the pairwise condition allows at most one ball of capacity one-half or greater.

9.1. All Capacities Below One-Half

Proposition 5.2 uses a smooth curve cut out by $n-1$ quadrics in complex projective space. The curve has positive genus for every $n\geq3$. Its normal directions yield a simplex of moments, with base area decreasing linearly as their sum grows. As the truncation approaches the half-capacity face, the model volume approaches $1/n!$. The auxiliary capacity simplices fit inside that truncation, so the common packing lemma applies.

9.2. One Large Ball in Real Dimension Eight or Higher

Proposition 5.3 reserves a central ball of capacity $a$, slightly larger than the large requested ball. The remaining balls have auxiliary capacities below $s=1-a$. The first normal model is a line over a hyperplane in projective space blown up at the center. The second comes from a curve cut out by quadrics inside the hyperplane. For $n\geq4$ that curve still has positive genus. Lifting the second model through the first gives a surface model of the exterior shell, with volume approaching $(1-a^n)/n!$.

9.3. One Large Ball in Real Dimension Six

The hyperplane construction would now produce a plane conic, which has genus zero. Proposition 6.7 instead starts with a quadric through the blowup point and uses a plane cubic with two marked points. A smooth plane cubic has genus one. This supplies the handle, and each excluded mark removes one logarithmic curvature mass from the reduced area.

Set $s=1-a$, $b=(2-a)/3$, and $t=p_1+p_2$. The limiting base area is

The two marks account for the coefficient 2. The slope changes from −7 to −9 at $t=s$, making the profile concave. Over the limiting domain $p_1,p_2\geq0$, $p_1\leq s$, and $t\leq b$, its integral is $(1-a^3)/6$, the shell volume. The actual packing uses a smaller domain that keeps the entire compact construction below the level needed for the cut.

10. Kähler Degenerations and Symplectic Transfer Into the Target Ball

Degeneration to the normal cone produces a family whose special fiber contains a projectivized normal-bundle component. This component exposes the toric regions where the area calculations are explicit. The volume estimates let the paper choose truncations large enough for the packing and still keep the compact regions away from the singular intersections of components. Symplectic parallel transport then moves those compact regions into nearby smooth fibers.

In dimension six, the transfer from the cubic component preserves the first circle moment exactly. Equivariance initially gives equality of the moment functions up to a constant. Both moments vanish on the corresponding fixed section, so the constant is zero. The transported region therefore stays below the cut level. The symplectic cut adds the divisor at that level while preserving the form in the part containing the packing.

Relative Moser isotopies let the proof identify the transferred models with the prescribed target forms while preserving the divisors that mark excluded regions. Removing the infinity divisor gives the open ball in the small-capacity case. In the large-ball cases, removing the exceptional divisor as well gives the exterior shell. The reserved margin separates the central source ball from the shell packing. Section 7 assembles the three cases, with all transfers defined on neighborhoods of the compact packing.

11. What the Lean Formalization Verifies and Where the Theorem Applies

OpenAI included the preprint and Lean development in its October 6 mathematics release. The family 343 scope note identifies the formalized statements as the full equivalence and the necessity direction. The Lean implementation’s top-level theorem combines strict volume and pairwise bounds in one direction and invokes the packing construction in the other. Its definitions use disjoint images of closed balls and symplectic maps on open neighborhoods. Lean checks the formal proof against its definitions and dependencies. Independent mathematical review evaluates the written argument and its context.

The criterion applies to finite families of positive-capacity standard balls and a standard ball target in real dimension at least six. Other target shapes, four-dimensional packings, and boundary contact under different embedding conventions require their own analysis. The result gives an existence test on capacities. The geometric proof builds embeddings through several auxiliary models and gives no performance benchmark for computing their coordinates.

For symplectic ball packing in dimensions six and higher, the theorem turns a geometric existence problem into two tests on capacities. The proof explains how the resulting slack can be spent, first across a surface and then in the target ball. Follow Binary Verse AI for more paper-by-paper explainers on symplectic geometry and formal proofs.