Imagine filling a space with identical spheres, each touching its neighbors but never overlapping. In two or three dimensions, you can sketch the scene. Now add five more directions, each at right angles to all the others. The picture stops helping. Yet mathematicians can still ask a precise question: how densely can spheres fill that space—and can any arrangement do better than a particular lattice?
For eight dimensions, the answer has been known since Maryna Viazovska’s breakthrough in 2016: the E8 lattice gives the densest possible packing. The new story is not that someone found a better arrangement or settled a lingering dispute. It is that researchers have translated the proof of this old result into a form a small computer program can check, one logical step at a time.
That shift—from the arrangement of spheres to the architecture of a proof—is the hidden landscape in a recent report by Sidharth Hariharan and colleagues. Their project’s milestone, reached in February 2026, is a formally verified proof that no sphere packing in eight-dimensional space can beat the E8 packing. The result was already accepted mathematics. The new question was whether its reasoning could be rebuilt inside a system that checks every inference.
To see why that is difficult, start with what the theorem must cover. It is not enough to compare a handful of candidate patterns. The claim ranges over every possible packing, including arrangements that do not repeat regularly. The researchers first had to teach their proof system what a packing means: a set of centers, a minimum separation between them, and a way to measure the fraction of space occupied as the region being examined grows larger and larger. Even the everyday word “densest” needs careful mathematical machinery when the arrangement could extend forever.
The route to an upper limit uses a surprising change of viewpoint. Instead of inspecting the spheres directly, the proof constructs a special function—a mathematical measuring device whose behavior constrains any possible packing. A result by Henry Cohn and Noam Elkies turns suitable functions into upper bounds on packing density. Viazovska found a function whose bound matches the density of the E8 arrangement exactly. Once the upper limit and the known packing meet, there is nowhere for a denser arrangement to hide.
That “magic” function is built from objects called modular forms, which have intricate symmetry rules. In the formal proof, these are not decorative advanced mathematics; they are the mechanism that makes the bound sharp. The function’s properties depend on complex analysis, Fourier transforms, and delicate integrals along contours. The team even had to choose specific rectangular paths for some integrals—not because the mathematics requires only rectangles, but because the proof library already had tools for reasoning about them. A human may glide over such a choice as routine. A formal system needs the choice spelled out and justified.
This is what formalization changes. In ordinary mathematics, a proof is written for readers who can fill in familiar steps, recognize standard results, and judge whether a sketch is convincing. In Lean, the theorem and every supporting claim are expressed in a strict language. A kernel checks that each step follows from earlier ones and the system’s foundations. It does not decide whether the argument is beautiful, useful, or the best way to understand the theorem. It checks whether the formal proof actually establishes the statement it claims to establish.
People did much of the groundwork before the automated system entered the final stretch. They defined sphere packings and density, built the mathematical infrastructure, formalized needed modular-form results, and laid out a detailed proof plan. The project’s human-written development was about 20,000 lines. Then an autoformalization model called Gauss worked from that existing blueprint and Lean code, completing a proof with no unfinished placeholders in five days. Its contribution expanded the project to 80,000 lines; a later refactoring pass reduced it to 60,000.
The scale is striking, but the line count is not the deepest result. The paper describes Gauss producing long, difficult arguments alongside routine steps that could have been handled more cleanly, sometimes repeating work already available in the library. The authors note that generating a proof was easier than turning it into concise, maintainable code. A proof that checks today can still be awkward to understand or reuse tomorrow. In mathematics, as in engineering, a working structure and a well-designed structure are not automatically the same thing.
There are also important boundaries around the achievement. The formal project follows a slightly modified proof blueprint rather than reproducing Viazovska’s original argument in every detail; notably, it uses Seewoo Lee’s proof of certain inequalities. The authors say the exact correspondence between Gauss’s large body of code and the intended proof path is still being investigated. So the milestone is a verified formal proof of the packing theorem—not a claim that a model independently discovered the theorem, or that every design goal for the project has been met.
Look back from the code and the familiar packing problem has acquired another dimension. There is the geometric space containing the spheres, and beneath it a second space: definitions, lemmas, contour arguments, and thousands of checked steps. In that hidden structure, a theorem can be inspected at a finer scale than ordinary prose usually allows. The challenge now is not merely to make proofs machine-checkable, but to make them readable and reusable too. The densest packing may be settled; the craft of building its proof so others can work with it is still unfolding.
