Symplectic ball packing in higher dimensions
From OpenAI Aftermath
Symplectic ball packing asks when several closed balls can be embedded disjointly and symplectically into a larger ball. Two obstructions are known in every dimension: the volume inequality and Gromov's two-ball obstruction, which says that the capacities of any two balls must sum to less than the capacity of the target. In dimension four further obstructions exist; Siegel and Yao conjectured that in real dimension at least six the two inequalities are the only ones. A manuscript in OpenAI's public mathematics collection (github.com/openai/math), dated 23 September 2026, claims this criterion for balls of arbitrary capacities, with a Lean formalization of the full statement. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- Gromov's pseudoholomorphic-curve method gives the two-ball obstruction in every dimension and further packing obstructions in dimension four; McDuff and Polterovich developed the connection with algebraic geometry, and Traynor and Schlenk developed explicit packing constructions, including higher-dimensional folding.
- Biran established packing stability for equal balls on closed rational symplectic four-manifolds; Buse and Hind extended equal-ball stability to higher-dimensional balls and to all closed rational symplectic manifolds, and Buse, Hind and Opshtein proved strong packing stability for small unequal balls on closed four-manifolds.
- Siegel and Yao formulated the higher-dimensional question for arbitrary capacities as their Conjecture A and studied stabilized packing problems.
The original result
- Claim. Theorem 1.1 of Symplectic Ball Packings in Higher Dimensions states that for integers n ≥ 3 and k ≥ 1 and positive capacities R, R1, …, Rk, the closed balls B2n(Ri) embed disjointly and symplectically into the interior of B2n(R) if and only if the sum of the Rin is less than Rn and Ri + Rj < R for every pair i ≠ j. Capacity is π times the squared Euclidean radius. The manuscript states that this resolves Siegel and Yao's Conjecture A positively and that in dimension four the two inequalities do not give a criterion.
- Method, as described: the construction uses a surface of positive genus as a base and a toric domain as a fiber, specified by a downward polytope in moment coordinates. The volume inequality makes the unused area of the base positive only on average; a Hamiltonian comparison lemma rearranges this area, a handle on the base surface stacks the balls in disjoint layers, and the resulting packing is transferred back to the target ball. Separate models treat the different capacity regimes, with a special construction in dimension six.
- Source (openai/math repository, commit
7ef5c0c): Symplectic Ball Packings in Higher Dimensions, dated 23 September 2026. - Formalization, as described by the repository. The scope note lean/docs/343.md states that the formalization proves the criterion in every symplectic dimension 2n with n ≥ 3, with each embedding defined on a neighbourhood of its closed source ball, and links two Comparator challenges: BallPacking.lean for the full equivalence and BallPackingNecessity.lean for the necessity direction.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 30 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | Symplectic ball packings in higher dimensions, an article of the Latent Seminar blog at lowrank.github.io | Reading (exposition) | Explains symplectic embeddings and capacity, necessity and elementary consequences, moment coordinates and area profiles, the Hamiltonian comparison from positive mean, how a handle converts the gap into disjoint layers, the models for the three capacity regimes and the six-dimensional shell, with proof outlines on the uniform rearrangement gap, the compactly supported primitive and the Moser vector field. | Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit 94c6630, 28 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full": the Lean main theorem states the equivalence for n ≥ 3, k ≥ 1 and positive capacities, with a packing defined as disjointly imaged smooth symplectic embeddings of open neighbourhoods of the closed balls into the open target ball, and the necessity challenge repeats the forward direction. It records a sandboxed Comparator pass for BallPacking and BallPackingNecessity. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 | cert-machine, openai/math lane K: run 38019899278, BallPacking, and run 38017370880, BallPackingNecessity | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept both solutions, in 3,489 s and 1,089 s; an earlier run of the full challenge did not finish. The project reports two-kernel certification of 398 of 416 challenges of the collection. | Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) lists neither challenge, so both were accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-19 | AI Proved What?, episode 343 Two tests are enough?, remade version of 23 October 2026 | Reading (exposition) | Video explainer of the claim and its history. The episode states that dimension four, where the statement is false, explicit embeddings and anything new about the easy direction are not claimed, gives as its own reading the consequence that two or more equal balls nearly fill the target exactly when there are at least 2n of them, and notes that the Lean development also proves Gromov's two-ball bound, which the paper only cites. | Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 27 October 2026: posted as a preprint: OpenAI, 43 pages, dated September 23, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: the full statement, both directions. The page states that it found no specialist comment, including from Siegel and Yao, and no reported error. |
Notes
- The background summarizes the manuscript's own account of earlier work.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
