Two tests are enough?
An AI preprint claims the Siegel–Yao ball-packing conjecture in every dimension from six up
Covers result 343 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.
3:27. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
A symplectic ball of capacity R is a round ball in even-dimensional space, measured by the area of its central disc. Can several closed balls be placed disjointly inside a bigger open ball by a map that preserves the symplectic structure? There are two obvious tests. Their volumes must add up to less, and, by Gromov’s work, any two balls must have capacities summing to less than the big one. In dimension 6, for 5 random balls, our computer finds the volume test passes 38 percent of the time, but the pairwise test only about 6 percent.
In 4 dimensions those two tests are not enough. 5 balls of capacity 0.42 pass both, yet a further obstruction from the conic through five points blocks them, as our computer checks. In 2023 Siegel and Yao conjectured that in dimension 6 and up, the two tests are the whole story. Before, this was known for one ball, for equal balls up to 2ⁿ of them, and for very many equal balls; the general case with unequal capacities in dimension 6 and up was open.
Result 343 is one OpenAI paper, 43 pages, dated September 23 and made public October 6, 2026. It claims the conjecture: in every dimension of at least 6, closed balls of any capacities fit disjointly into an open ball exactly when the volume test and the pairwise test both pass. One consequence, by our own reading: two or more equal balls can fill nearly all of the big ball exactly when there are at least 2ⁿ of them.
What it doesn’t claim
Not claimed: dimension 4, where the statement is false; explicit embeddings, since the construction is an existence argument; or anything new about the easy direction, which follows from volume and Gromov’s bound.
Where it stands
- Posted as a preprint
- OpenAI, 43 pages, dated September 23, 2026
- Peer reviewed
- Not yet
- Formalized in Lean
- The full statement, both directions (docs)
Last checked October 19, 2026. The paper is unrefereed and unchanged since release. Lean formalizes the full statement, both directions, in about 200 files and 107,000 lines, not run by us; three outside projects re-ran it and it passed, one also with a second kernel. The Lean appears to follow the paper’s plan, and also proves Gromov’s two-ball bound, which the paper only cites. We found no specialist comment, including from Siegel and Yao, and no reported error. OSVerify has not reviewed it.
How the proof goes
- Fibre over a curve with a handle. At most one ball can have capacity at least half the target. The paper degenerates projective space to a model fibered over a curve with a handle, reserving the large ball, if there is one, at the center. In dimension 6, with a large ball, the natural curve has no handle, so the paper uses a plane cubic with two marked points instead; our computer confirms its area integrals exactly for sample sizes.
- Positive on average, negative at the core. The volume test only makes the unused area positive on average; near the core it can be negative, as our computer shows for 20 balls of capacity 0.35. A Hamiltonian comparison lemma rearranges the area, the handle stacks the balls in disjoint layers, and a transfer argument carries the packing back to the ball.
The numbers in the video
- Ours: in dimension 6, for five random balls, the volume test passes 38% of the time and the pairwise test only about 6%.
- Ours: in dimension 4, five balls of capacity 0.42 pass both tests (0.88 and 0.84) but fail the conic bound (2.1, not below 2).
- Ours: by our reading of the claim, k equal balls fill at best min(1, k/8) of a 6-dimensional ball, against the dimension-4 values 1, 1/2, 3/4, 1, 4/5, 24/25, 63/64, 288/289.
- Lean: 207 files and 107,119 lines in the import closure of the two comparators (counted by us; not run by us).
Read the source
- Symplectic Ball Packings in Higher Dimensions (PDF), 43 pages.
- The Lean formalization notes.
- The collection’s catalog, where this is result 343.
The paper
OpenAI groups related papers into one result; this one has a single paper.
Transcript
Read the full script
0:00The question
A symplectic ball of capacity R is a round ball in even-dimensional space, measured by the area of its central disc. Can several closed balls be placed disjointly inside a bigger open ball by a map that preserves the symplectic structure? There are two obvious tests. Their volumes must add up to less, and, by Gromov’s work, any two balls must have capacities summing to less than the big one. In dimension 6, for 5 random balls, our computer finds the volume test passes 38 percent of the time, but the pairwise test only about 6 percent. In 4 dimensions those two tests are not enough. 5 balls of capacity 0.42 pass both, yet a further obstruction from the conic through five points blocks them, as our computer checks. In 2023 Siegel and Yao conjectured that in dimension 6 and up, the two tests are the whole story. Before, this was known for one ball, for equal balls up to 2ⁿ of them, and for very many equal balls; the general case with unequal capacities in dimension 6 and up was open.
1:08The claim
Result 343 is one OpenAI paper, 43 pages, dated September 23 and made public October 6, 2026. It claims the conjecture: in every dimension of at least 6, closed balls of any capacities fit disjointly into an open ball exactly when the volume test and the pairwise test both pass. One consequence, by our own reading: two or more equal balls can fill nearly all of the big ball exactly when there are at least 2ⁿ of them. Not claimed: dimension 4, where the statement is false; explicit embeddings, since the construction is an existence argument; or anything new about the easy direction, which follows from volume and Gromov’s bound.
1:55How the proof goes
At most one ball can have capacity at least half the target. The paper degenerates projective space to a model fibered over a curve with a handle, reserving the large ball, if there is one, at the center. In dimension 6, with a large ball, the natural curve has no handle, so the paper uses a plane cubic with two marked points instead; our computer confirms its area integrals exactly for sample sizes. The volume test only makes the unused area positive on average; near the core it can be negative, as our computer shows for 20 balls of capacity 0.35. A Hamiltonian comparison lemma rearranges the area, the handle stacks the balls in disjoint layers, and a transfer argument carries the packing back to the ball.
2:42Where it stands
The paper is unrefereed and unchanged since release. Lean formalizes the full statement, both directions, in about 200 files and 107,000 lines, not run by us; three outside projects re-ran it and it passed, one also with a second kernel. The Lean appears to follow the paper’s plan, and also proves Gromov’s two-ball bound, which the paper only cites. We found no specialist comment, including from Siegel and Yao, and no reported error. If it holds, in dimension 6 and up, balls pack into a ball exactly when volume and the two-ball rule allow: a clean answer that fails in dimension 4.
Spot a mistake?
This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.