An AI moves a bound untouched since 1978 — and what is still wide open
Sphere packing keeps two scoreboards. On one side are lower bounds: somebody builds an arrangement, or proves one must exist, and the record rises. On the other are upper bounds: somebody proves that no arrangement, however ingenious, can beat a certain density, and the ceiling falls. The true answer is trapped between them. Close the two and the problem is solved.
Both scoreboards had been stuck for a very long time. The upper bound had not moved since 1978. The shape of the lower bound had not moved since 1947. Then, within a year of each other, both moved. In 2025 Bo’az Klartag found a construction that beats seventy-eight years of records by a factor proportional to the dimension. In 2026 an AI model produced the first improvement to the general upper-bound exponent since 1978, together with a proof written in a language a computer can check line by line.
This lesson looks at what those two results are, what they are worth, and how much of the problem is still standing afterwards. The short answer to the last question is: nearly all of it.
Densities in high dimensions are quoted as 2−c·n, and the whole contest reduces to the number c. The chart below plots it. Constructions have always given c = 1: Minkowski in 1905, Rogers in 1947, Ball in 1992 and Klartag in 2025 all produce densities of the form poly(n)·2−n, so all four sit on the same line, and the century of progress between them shows up only in the polynomial written beside each dot. Proofs give the other side, and there has only ever been one line: the Kabatianskii–Levenshtein bound of 1978, which fell to 0.6044005 in 2026.
The shaded band between the two is the region the true density has never been driven out of. Watch what it does as the timeline runs. It does not close, it does not narrow to a sliver, it does not visibly change at all. That is the honest picture of the field.
The first improvement to the general upper bound exponent since 1978, pinning the exact asymptotic limit of the Cohn–Elkies method at e/2π.
The exponent axis is the only scale on which four centuries of results are comparable: every lower bound ever proven has the form poly(n)·2−n, so all four sit on the same cyan line at c = 1, and the improvements from 1905 to 2025 show up only in the prefactor printed beside each dot. The upper bound arrived in 1978 and moved once, in 2026, by 0.0053. The time axis is deliberately warped — sixty per cent real elapsed time, forty per cent even spacing — so that the modern cluster stays legible without hiding the 220-year silence after Kepler.
Try it: Press Play and watch four centuries go by in half a minute, or jump straight to a year with the chips. Keep an eye on the gap readout at the bottom: when the upper bound first appears in 1978, the two bounds differ by a factor of 2391 in dimension 1,000. After the breakthroughs of 2025 and 2026 they differ by 2377. Forty-eight years of work, two of them record-breaking, narrowed the gap by under four per cent.
It is worth being precise about what Klartag did, because it is the larger of the two results by most measures and it is easy to let the machine story swallow it. Rogers’ 1947 argument grows an ellipsoid inside a lattice and reads off a density of roughly c·n·2−n. Ball improved the constant in 1992. Nobody improved the shape — for seventy-eight years.
Klartag’s 2025 paper grows the ellipsoid by a stochastic rule instead of a deterministic one, and the average over that randomness gains an entire extra factor of n, giving c·n²·2−n. In dimension 1,000 that is a thousandfold improvement on the previous record; in dimension a million, a millionfold. It is the largest single advance on the lower bound since the Second World War, and it came from one person thinking about ellipsoids.
And it did not move the exponent. Both the new record and the old one are 2−n multiplied by a polynomial; a polynomial is nothing against an exponential. This is not a criticism of the result. It is the measure of how hard the problem is: the best improvement in seventy-eight years leaves c exactly where it was.
Plot both sides as exponents and the state of knowledge becomes uncomfortably clear. The upper bounds sit near 0.60. The lower bounds climb toward 1. Between them is a band that no result has ever entered, and because these are exponents, the band is not a margin of error — it is a factor of 2 to the power of several hundred in any dimension worth caring about.
One caution matters more than any other on this chart. Every curve here is asymptotic: each is a claim about behaviour as n → ∞, carrying an unspecified constant or a factor that disappears only in the limit. Evaluated in small dimensions the formulas do not merely become imprecise, they become false — the 1978 upper bound, taken literally at n = 24, sits far below the density the Leech lattice actually achieves. Nothing is plotted below dimension 100, and the caption under the chart says why.
Why the chart starts at 100. Every curve here is asymptotic: each is a statement about the exponent as n → ∞, carrying an unspecified constant or a (1 + o(1)) that vanishes only in the limit. Evaluate the 1978 upper bound at n = 24 and it returns 4.70 × 10⁻⁵, which is about 41 times smaller than the density the Leech lattice demonstrably achieves. The formula is not wrong — it simply says nothing at n = 24, and plotting it there would be a lie drawn to scale.
Read the axis as density: smaller c means denser, so upward is better packing. After the two headline results of 2025 and 2026, the densest possible packing in dimension 1,000 is known to lie somewhere between 2−0.6044005n and roughly 2−n. That is not a near miss. It is a window 2³⁷⁷ wide, and it has been widening, not narrowing, with every dimension you add.
Try it: In the full range, drag the dimension slider and watch the window readout grow — it is wider in dimension 5,000 than in dimension 500, because the gap is exponential in n. Then switch to Zoom the upper bounds, which magnifies a strip 0.012 wide. Only at that magnification do the 1978 and 2026 lines separate at all.
The 2026 result is easy to describe wrongly, so here it is described carefully. It did not discover a denser packing. It did not solve a dimension. What it did was settle the exact asymptotic behaviour of the Cohn–Elkies linear programming bound, the technique behind nearly every serious upper bound in the subject, including Viazovska’s proofs in dimensions 8 and 24. The limit turns out to be e/(2π) ≈ 0.4326, and knowing it exactly fixes the best density exponent the method can deliver at 0.6044005, up from the 1978 record of 0.5990558.
That single number does two jobs at once. It is an improvement — the first to this exponent in forty-eight years. It is also a ceiling on a proof technique: because the limit is exact rather than approximate, no future refinement of linear programming, no better test function and no larger computation, can ever push past it. The most productive tool in the field has been measured, and it is finite. Beating 0.6044005 will require an idea that is not linear programming at all.
It found no packing. Not one sphere was moved, no dimension was solved, and the densest arrangement known in any dimension is exactly what it was the day before.
It determined the exact asymptotic limit of the Cohn–Elkies linear programming bound: LPd1/d → e/(2π) ≈ 0.4326 as d → ∞.
A density exponent of 0.6044005, up from 0.5990558 — and simultaneously a ceiling: no argument of this family, however cleverly built, can ever do better.
The whole result is that arrow. Everything downstream of it — the new exponent, and the proof that the method can never beat it — follows from knowing the limit exactly rather than approximately.
Both readings are honest and they point in opposite directions. As a fraction of the exponent the gain is 0.89% — the yellow sliver above, barely wide enough to see. As a fraction of the densities involved it is 20.0053447·n, which in dimension 1,000 means the 2026 bound forbids 40.6 times more density than the 1978 bound did. A tiny move in an exponent is never a tiny move.
On verification. This result shipped as one of ten, each with a proof written in Lean 4 and published in a public repository, openai/ten-proofs. A Lean proof that compiles has been checked line by line by a machine whose logic is itself checked, which is a stronger guarantee than most published mathematics carries. It is not the same thing as acceptance by the mathematical community: at announcement none of the ten had been through conventional peer review, and what a referee supplies — that the statement proved is the statement that matters, that the definitions say what they appear to say, that the result belongs in the literature — is not something a proof checker is asked to do. Both facts are worth holding at once.
Try it: Drag the dimension slider and watch the two readings disagree. The exponent moves by 0.89% and the yellow sliver on the bar stays nearly invisible — yet in dimension 5,000 the new bound forbids about 108 times more density than the old one. Both numbers describe the same result. Quoting only one of them would be a choice, not a summary.
The verification story deserves the same care. The result arrived as one of ten, each accompanied by a proof written in Lean 4 and published openly. A Lean proof that compiles has been checked by a program whose own logic is checked, which rules out the ordinary failure mode of a subtly broken step. That is a real and unusually strong guarantee. It is also a different thing from acceptance by the mathematical community: at announcement the results had not been through conventional peer review, and a referee is asked for things a proof checker is not — whether the theorem stated is the theorem that matters, whether the definitions mean what they appear to mean, whether the work belongs in the literature. Machine-checked and accepted are both worth having, and they are not the same status.
After the best year the subject has had in decades, here is the state of the record books. Optimal packings are proven in five dimensions. Dimension 4 is not among them. Nobody knows whether the densest high-dimensional packings are ordered or disordered. The kissing number in dimension 5 is known only to be between 40 and 44. And the exponent gap — the question underneath all the others — is as wide as it has ever been.
D₄ fills π²/16 ≈ 61.69% of four-dimensional space. Korkine and Zolotareff showed in the 1870s that no lattice does better, and there the matter has stood. A packing does not have to be a lattice, and ruling out every irregular arrangement is precisely the step that took Thomas Hales six years of computer-assisted work in dimension 3, and another twelve to formalise. No comparable programme exists for dimension 4.
The strangeness is that the neighbouring question in the same dimension is finished. The kissing number in four dimensions is 24, settled by Musin in 2003. How many spheres can touch one is known exactly; how densely they can be laid out is not known at all.
Four hundred and fifteen years after Kepler, the densest packing of equal spheres is proven in exactly 5 dimensions — 1, 2, 3, 8 and 24 — out of infinitely many. Every other dimension has a champion and no verdict. That is not a gap in the literature waiting to be tidied up; it is the honest state of one of the oldest questions in mathematics.
Try it: Open the dimension 4 card first. The kissing number there was settled in 2003 and the packing problem beside it is wide open — two questions in the same dimension, one finished and one untouched. Then open the last card for the sharpest consequence of the 2026 result: dimensions 8 and 24 are not the start of a pattern, and the method that solved them provably cannot solve the rest.
It is tempting to read 2025 and 2026 as the moment the problem started to give way, and just as tempting to read them as proof that nothing much changed. Neither is right. A human found the largest construction improvement in seventy-eight years by thinking hard about the shape of an ellipsoid. A machine measured a proof technique exactly and, in doing so, both improved it and retired it. Two genuine results, arrived at two completely different ways, in the space of a year.
What they have in common is more interesting than where they came from. Both moved the boundary of the known without touching the thing in the middle. The true density in high dimensions is still pinned only between 2−n and 2−0.6044005·n, a window so wide that stating it in dimension 1,000 requires an exponent of its own. The oldest question in the subject — how densely can equal spheres fill space — has an exact answer in five dimensions and an exponentially large range of possible answers everywhere else.
Kepler wrote his conjecture down in 1611 and did not think it needed a proof. It took 387 years to get one. The lesson of the four centuries since is not that the problem is about to fall, to a person or to a machine, but that it has been consistently harder than anyone expected — and that it keeps rewarding whoever is willing to look at an old argument and ask what it would take to move it by one more factor of n.