The Cannonball Stack – Kepler and Flyspeck

In the bitter winter of 1611, Johannes Kepler gazed at a fragile six-cornered snowflake melting on the sleeve of his coat as he crossed the Charles Bridge in Prague. Contemplating the geometric packing of tiny water particles that gave the snowflake its hexagonal symmetry, Kepler turned his thoughts to a practical question posed to him by the English mathematician and explorer Thomas Harriot: how should a naval gunner stack cannonballs in the hold of a warship to cram the greatest possible number into the smallest possible space? Kepler asserted that the common grocery-store pyramid—the face-centered cubic arrangement used by grocers to stack oranges—was mathematically insurmountable: no arrangement of equal spheres in three-dimensional space could achieve a packing density exceeding π / square root of 18, or roughly seventy-four percent. Yet for nearly four centuries, that intuitive claim resisted every effort of human proof. When American mathematician Thomas Hales finally conquered it in 1998 using hundreds of pages of mathematics and gigabytes of computer calculations, the international peer-review system collapsed under the sheer volume of code, confessing it was only ninety-nine percent certain. Refusing to leave an asterisk on his life’s work, Hales launched the Flyspeck Project, embarking on an epic eleven-year campaign to formalize and machine-verify every single logical deduction inside computer proof assistants. The completion of Flyspeck not only settled Kepler’s four-hundred-year-old riddle, but inaugurated the era of machine-certified truth in mathematics.

1. The Gunner’s Riddle – Harriot, Raleigh, and the Six-Cornered Snowflake

The origin of the sphere packing problem was not born in the cloistered halls of pure academia, but on the high seas during the Elizabethan age of exploration. In the late 1580s, Sir Walter Raleigh, preparing naval expeditions to the New World, tasked his scientific advisor, the brilliant mathematician and astronomer Thomas Harriot, with developing quick mathematical formulas for naval quartermasters. When looking at a massive pyramid of iron cannonballs piled on a wooden ship deck, could a gunner instantly determine the exact count of cannonballs without counting them one by one?

Harriot solved the counting formulas effortlessly, discovering triangular and square pyramidal number sequences. But in doing so, Harriot became fascinated by a deeper structural question: what was the densest possible way to pack spherical objects into space? Harriot corresponded with Johannes Kepler, the Imperial Mathematician to the Holy Roman Emperor Rudolf II in Prague.

In 1611, Kepler published a delightful, visionary essay titled “Strena Seu de Nive Sexangula” (A New Year’s Gift of the Six-Cornered Snowflake), presented as a gift to his patron Johannes Matthäus Wacker von Wackenfels. In this short treatise—widely regarded as the founding document of crystallography—Kepler investigated why snowflakes always exhibit six-fold hexagonal symmetry. He modeled the problem by studying how spherical pellets pack together in a plane.

In two dimensions, the densest packing of equal circles is the familiar hexagonal honeycomb pattern, where every circle is surrounded symmetrically by six neighbors. In this triangular lattice arrangement, the circles occupy a fraction of the plane equal to.

Kepler then considered three dimensions. Starting with a flat hexagonal layer of spheres, a second layer can be placed into the hollows (interstices) between the spheres of the first layer. When adding a third layer, there are two distinct choices: one can place the spheres directly above the spheres of the first layer (yielding the hexagonal close-packed or HCP lattice, with an ABABAB… stacking sequence), or one can place them over the remaining unoccupied hollows of the first layer (yielding the face-centered cubic or FCC lattice, with an ABCABC… stacking sequence).

Both the FCC and HCP arrangements yield an identical, remarkable packing density.

In his 1611 treatise, Kepler stated with absolute conviction that no arrangement of equal spheres in three-dimensional Euclidean space could ever achieve a density greater than π / square root of 18. This simple, elegant assertion became known to history as the Kepler Conjecture.

2. The Non-Lattice Nightmare – Why Intuition Failed for Four Centuries

To an observer stacking oranges or cannonballs, the Kepler Conjecture feels intuitively self-evident. How could any disordered, chaotic jumble of spheres possibly pack tighter than the crystalline symmetry of the face-centered cubic lattice? Yet in mathematics, intuitive obviousness is frequently an illusion that conceals treacherous analytical traps.

The first major breakthrough came in 1831, when Carl Friedrich Gauss proved that the Kepler Conjecture is strictly true if one restricts attention exclusively to regular lattice packings. A lattice packing is an arrangement where the centers of the spheres form a discrete subgroup of real space (a repeating crystallographic grid). Gauss demonstrated that among all possible three-dimensional lattices, the face-centered cubic lattice achieves the absolute maximum density.

However, Gauss’s theorem left a massive, terrifying loophole: what about non-lattice packings? A packing of spheres does not have to be a regular repeating lattice. It can be completely irregular, disordered, quasi-crystalline, or locally fractured. In fact, in local geometry, disordered configurations can achieve packing densities that appear to exceed the FCC lattice!

Consider twelve spheres surrounding a central sphere. If one places the twelve outer spheres into the face-centered cubic configuration, there is noticeable slack: the outer spheres do not touch each other tightly. In 1952, British mathematician H.S.M. Coxeter observed that if one arranges twelve spheres in the vertices of a regular icosahedron around a central sphere, the arrangement is significantly tighter locally than the FCC arrangement. The icosahedral arrangement achieves an astonishing local density.

However, icosahedral symmetry is mathematically impossible to tile through three-dimensional Euclidean space! Because five-fold rotational symmetry cannot tile real space, any attempt to extend icosahedral packing outward introduces severe geometric frustration: gaps, voids, and misalignments inevitably emerge in the second and third shells of spheres, driving the average global density down. The central nightmare of the Kepler Conjecture was that some clever, highly complex non-periodic arrangement—perhaps an exotic quasi-crystal or an intricate fractal labyrinth—might achieve an ultra-dense local packing that avoids macroscopic voids, edging past seventy-four percent.

Proving that no such arrangement could exist anywhere in the infinite expanse of real space required bounding the packing density across an uncountable infinity of possible spatial configurations. For centuries, every analytical tool of classical geometry and calculus failed to conquer this infinite-dimensional optimization space.

3. The Fejes Tóth Blueprint – Dissecting Space into Polyhedral Cells

The conceptual path out of the wilderness was cleared in 1953 by the Hungarian geometer László Fejes Tóth. Fejes Tóth proposed a revolutionary blueprint: rather than attempting to analyze the infinite expanse of space all at once, the problem could be reduced to a finite, localized geometric optimization problem over polyhedral decomposition cells.

Fejes Tóth utilized the concept of a Voronoi cell. Given a discrete configuration of sphere centers C = {x_1, x_2,…} in real space, the Voronoi cell (V(x_i)) of a sphere center x_i is the region of space consisting of all points that are closer to x_i than to any other sphere center in the packing.

Voronoi cells are convex polyhedra that tile three-dimensional space completely without gaps or overlaps. The local packing density of a sphere of radius r within its Voronoi cell is simply the volume of the sphere divided by the volume of the polyhedron.

Fejes Tóth suggested that if one could prove that the volume of every Voronoi cell (or a suitably modified decomposition cell) is bounded below by a specific geometric constant corresponding to the FCC dodecahedron, the global density bound would follow immediately by summation. He famously remarked that with the advent of high-speed electronic digital computers, it might be possible to turn this geometric decomposition into a finite, exhaustive computational algorithm.

4. Thomas Hales and the Computational Sledgehammer

In 1992, Thomas Hales, a young associate professor at the University of Michigan, decided to take Fejes Tóth’s blueprint seriously. Recognizing that standard Voronoi cells were computationally unwieldy because distant spheres could alter the cell boundaries, Hales invented a refined spatial partition known as the Q-system (and later the D-system), decomposing space around each sphere into a mixture of simplices and polyhedral fragments based on Delaunay triangulations.

Hales formulated a precise non-linear score function (S(D)) representing the volume deficit of each decomposition cluster. The Kepler Conjecture was equivalent to showing that the total score of any valid cluster of spheres could never drop below the score achieved by the face-centered cubic lattice. To prove this, Hales and his brilliant doctoral student Samuel Ferguson launched a monumental computational campaign:

1. Graph-Theoretic Classification: The first stage was purely combinatorial. Any potential counterexample to the Kepler Conjecture would correspond to a cluster of neighboring spheres whose contact graph forms a planar graph. Hales and Ferguson wrote automated algorithms to generate and classify every possible planar graph satisfying strict geometric criteria. The algorithm exhaustively produced over 5,000 candidate planar graphs representing all possible packing topologies that could theoretically beat FCC.
2. Linear Programming Bounds: For each candidate graph, the geometric constraints—sphere radii, edge lengths, dihedral angles, and solid angles—generated a complex system of inequalities. Hales formulated these constraints as massive linear programming problems. Over 100,000 distinct linear programming problems were solved on computer clusters to bound the score of thousands of candidate graphs, proving that the vast majority were geometrically impossible.
3. Non-Linear Optimization via Interval Arithmetic: For the remaining several hundred stubborn graphs that could not be eliminated by linear approximations, Hales and Ferguson had to solve non-linear optimization problems over multi-dimensional domains. To ensure mathematical rigor and prevent floating-point rounding errors from invalidating the proof, they implemented rigorous interval arithmetic. Instead of computing with standard floating-point numbers, every calculation tracked intervals [a, b] containing the true real values, with rounding modes explicitly controlled toward positive and negative infinity.

In August 1998, after six years of relentless calculation, Thomas Hales and Samuel Ferguson announced the completion of the proof. The Kepler Conjecture was true: no arrangement of equal spheres could ever achieve a density greater than π / square root of 18. The proof spanned nearly 300 pages of dense mathematical manuscripts, accompanied by over 3 gigabytes of computer code, geometric data tables, and numerical output logs.

5. The Peer-Review Crisis – Ninety-Nine Percent Certain

Hales submitted the monumental manuscript to the world’s most prestigious mathematical journal, the Annals of Mathematics. The editorial board was confronted with an unprecedented dilemma. How could an academic journal verify a mathematical proof whose validity depended not merely on traditional prose deductions, but on the flawless execution of thousands of lines of custom C++ and Fortran code, complex linear programming solvers, and billions of floating-point interval evaluations?

The Annals took an unprecedented step: they assembled a special twelve-person panel of international experts in discrete geometry, optimization, and computer science, headed by Gábor Fejes Tóth (the son of László Fejes Tóth). The panel met in special seminars, scrutinized manuscripts, analyzed algorithms, and ran independent verification scripts.

The review process dragged on for one year, two years, three years, and finally four years. The referees became physically and intellectually exhausted. While they were able to verify the theoretical mathematical architecture developed by Hales, they found it humanly impossible to verify every single computer program, every compiler optimization flag, every hardware instruction set, and every line of custom script code. There was simply no mechanism in human peer review to guarantee that a microscopic software bug, memory leak, or logic error had not corrupted a single calculation among the hundreds of thousands of optimization runs.

In 2003, after five years of agonizing labor, Gábor Fejes Tóth delivered the panel’s historic verdict to the editors of the Annals. The referees stated that they were “99% certain” that Hales’s proof was correct, but they could not certify the computer calculations. The editorial board made an agonizing decision: they agreed to publish the theoretical, mathematical portion of Hales’s paper in the Annals of Mathematics (which appeared in 2005), but accompanied by an explicit editorial disclaimer stating that the computer calculations had not been fully verified. The computational details were relegated to a sister publication, Discrete & Computational Mathematics.

6. The Birth of the Flyspeck Project – An Audacious Vow

For most mathematicians, publication in the Annals of Mathematics with 99% certainty would have been celebrated as the crowning triumph of a career. For Thomas Hales, it was an intolerable wound. In mathematics, 99% certainty is an oxymoron: a mathematical proof is either logically certain, or it is not a proof at all. Hales refused to allow the Kepler Conjecture to stand in the history books with an eternal asterisk.

In 2003, Hales made an audacious public vow: he would re-prove the Kepler Conjecture from scratch, formalizing every single deduction, every equation, every graph, and every interval computation inside interactive theorem provers. Every line of logic would be certified down to the foundational axioms of mathematical logic, where verification is performed by a tiny, tamper-proof proof-checking kernel whose code consists of only a few hundred lines of verified logic.

Hales named his grand undertaking the Flyspeck Project. The name was a clever acronym derived from F-P-K-C (Formal Proof of the Kepler Conjecture), while paying homage to the English idiom “to flyspeck”—meaning to examine something with obsessive, microscopic scrutiny to detect the tiniest imperfection.

When Hales announced Flyspeck, the broader mathematical establishment was profoundly skeptical. Formalizing even simple mathematical theorems in proof assistants like HOL Light, Coq, or Isabelle was notoriously laborious: a one-page textbook proof often required months of tedious formalization. Many prominent mathematicians predicted that formalizing a 300-page proof containing 100,000 non-linear optimization problems would require centuries of human labor, dismissing Flyspeck as a quixotic, impossible fantasy.

7. The Architecture of Formalization – HOL Light and Isabelle

To execute the Flyspeck Project, Thomas Hales assembled an international coalition of mathematicians and computer scientists, including John Harrison (the creator of HOL Light and an expert on floating-point formal verification at Intel), Mark Adams, Cezary Kaliszyk, Roland Zumkeller, Alexey Solovyev, and Josef Urban.

The team selected two primary interactive theorem provers based on higher-order logic: HOL Light and Isabelle/HOL. Both systems are built on the strict LCF architecture conceived by Robin Milner: every theorem must be certified by a tiny, trusted logical kernel consisting of a handful of primitive inference rules (such as modus ponens, reflexivity, and substitution). No matter how large or complex a mathematical library becomes, no statement can be accepted as true unless the kernel generates a formal deduction chain from the foundational axioms.

The formalization of the Kepler Conjecture required conquering four distinct, massive challenges:

1. The Core Geometric and Trigonometric Library: Developing a complete, formalized library of three-dimensional Euclidean geometry in HOL Light. Hundreds of foundational lemmas concerning vectors, matrices, dot products, cross products, convex hulls, polyhedra, solid angles, and spherical trigonometry had to be rigorously formalized from scratch.
2. Formalizing Graph Theory and Planar Tesselations: Proving the combinatorial classification of candidate planar graphs. Tobias Nipkow and Gertrud Bauer formalized the planarity algorithms in Isabelle/HOL, verifying that the computer program that enumerated the 5,000 planar graphs was formally correct and that no possible candidate graph had been omitted.
3. Formal Linear Programming: Developing a verified linear programming certificate checker. Alexey Solovyev and Thomas Hales formalized duality theory in linear programming. Rather than formalizing the complex simplex algorithm itself, they used standard commercial solvers to compute duality certificates (dual multipliers), and then used the HOL Light kernel to rigorously verify that the dual multipliers proved the bounds, reducing thousands of hours of computation to instant, machine-checked certifications.
4. Rigorous Formal Interval Arithmetic: Formalizing the non-linear optimization bounds. Roland Zumkeller and Alexey Solovyev built a formal interval arithmetic engine within HOL Light. Every mathematical function—including sines, cosines, square roots, and arctangents—was approximated by rigorous Taylor series polynomials with machine-verified remainder error terms, proving that no rounding error could compromise the bounds.

8. The 2014 Triumph – Absolute Logical Certainty

For eleven years, the Flyspeck team labored with relentless discipline. Thousands of lemmas were formalized, git repositories grew to millions of lines of proof scripts, and computational jobs ran for weeks on server clusters across the globe.

In August 2014—exactly sixteen years after Hales originally announced his computer-assisted proof—Thomas Hales announced that the Flyspeck Project was complete. Every single step of the proof of the Kepler Conjecture had been completely formalized and verified by the logical kernels of HOL Light and Isabelle. The computational verification ran to completion without a single error.

The resulting formal proof comprised over 500,000 lines of formal computer code. In 2017, the complete, definitive formal proof was published in the journal Forum of Mathematics, Pi, authored by Thomas Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Hoai Thi Ta, Nam Trung Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, and Roland Zumkeller.

The asterisk was gone. Four hundred and three years after Johannes Kepler contemplated the snowflake on the Charles Bridge, the Kepler Conjecture stood as an indisputable mathematical theorem, verified with the highest standard of certainty human civilization has ever achieved.

9. The Dimension of Magic – Maryna Viazovska and the E8 Lattice

While the three-dimensional Kepler Conjecture was conquered through the brute computational sledgehammer of Flyspeck, the sphere packing problem possessed an unexpected, luminous dimension of pure analytical magic that would stun the mathematical world just two years later.

What happens to sphere packing in higher dimensions? In general dimensions d, the problem is notoriously difficult. As dimension increases, space becomes intensely “empty”: the volume of a sphere relative to the bounding cube enclosing it plunges exponentially toward zero. Finding dense packings becomes an agonizing challenge. However, mathematicians noticed two extraordinary exceptions: dimension 8 and dimension 24.

In dimension 8, there exists a crystalline lattice of supernatural perfection: the E_8 lattice, associated with the exceptional Lie group E_8. In dimension 24, there exists the legendary Leech lattice Lambda_24, discovered by John Leech in 1965, intimately connected to the Golay code and the Monster sporadic group. In both dimensions, these lattices pack spheres with breathtaking density.

In 2003, Henry Cohn and Noam Elkies developed a powerful linear programming bound for sphere packing based on Fourier analysis. The Cohn-Elkies method proved that if one could construct a specific “magic function” (f(x)) satisfying precise positivity conditions both in spatial coordinates and under the Fourier transform, one could prove that a given lattice is the densest possible packing in that dimension. For thirteen years, mathematicians searched in vain for the exact analytical formulas for the magic functions in dimensions 8 and 24.

In March 2016, a thirty-one-year-old Ukrainian mathematician at the Swiss Federal Institute of Technology in Lausanne (EPFL) named Maryna Viazovska uploaded a stunning twenty-three-page paper to the arXiv: “The sphere packing problem in dimension 8.” Working alone, Viazovska explicitly constructed the exact magic function for dimension 8 using the theory of modular forms and quasimodular forms, specifically Eisenstein series and theta functions!

Just one week later, Viazovska, collaborating with Henry Cohn, Abhinav Kumar, Stephen D. Miller, and Danylo Radchenko, extended her modular form techniques to dimension 24, proving that the Leech lattice is the absolute densest packing in twenty-four dimensions. In stark contrast to Hales’s 500,000 lines of Flyspeck code, Viazovska’s proof was a compact, exquisite symphony of classical analysis that could be checked by hand in an afternoon. For this magnificent breakthrough, Maryna Viazovska was awarded the Fields Medal in 2022.

11. The Cohn-Elkies Bound – Fourier Analysis and Poisson Summation

To understand the profound analytical contrast between the algorithmic verification of Flyspeck and Maryna Viazovska’s breakthrough in dimensions 8 and 24, one must explore the harmonic machinery established in 2003 by Henry Cohn and Noam Elkies. Cohn and Elkies revolutionized higher-dimensional discrete geometry by adapting the linear programming bounds of Philippe Delsarte—originally developed for error-correcting codes—to the continuous domain of Euclidean space via the Poisson Summation Formula.

The Poisson Summation Formula is one of the most powerful identities in harmonic analysis. For any geometric lattice filling multidimensional space and any well-behaved, rapidly decaying test function, the sum of the function values evaluated across every lattice point precisely equals the sum of its Fourier transform across the reciprocal dual lattice, scaled by the cell volume.

where the Fourier transform is normalized as.

Cohn and Elkies made a brilliant deduction. Suppose one can find a radial Schwartz function (f(x) = f_0(|x|)) that satisfies three strict conditions:

1. The function and its Fourier transform are strictly positive at the origin.
2. Beyond the sphere diameter, the function remains zero or strictly negative at all distances.
3. Across all frequencies, its Fourier transform remains strictly non-negative.

If such a “magic function” exists, Cohn and Elkies proved that the maximum possible sphere packing density delta_d in dimension d is strictly bounded above by.

This linear programming bound holds universally for all sphere packings—whether they are regular lattices or wildly disordered, non-periodic arrangements! By searching for optimal test functions using numerical optimization and polynomials multiplied by Gaussians, Cohn and Elkies computed upper bounds in various dimensions. In dimensions 8 and 24, their numerical upper bounds matched the known densities of the E_8 lattice and the Leech lattice to an astonishing thirty decimal places! This near-miraculous agreement convinced the mathematical community that the Cohn-Elkies bound was sharp in dimensions 8 and 24, but proving it required finding the exact, analytical closed-form formula for the magic function.

12. Viazovska’s Architecture – Modular Forms and Integral Transforms

For thirteen years, the exact formula for the Cohn-Elkies magic function eluded the world’s greatest analysts. Numerical approximations suggested that for the bound to be exact, the magic function (f(r)) for the E_8 lattice had to possess forced double zeros at all non-zero lattice vector lengths: r = square root of 2, square root of 4, square root of 6, square root of 8,…, while its Fourier transform (f(k)) had to possess double zeros at identical locations. Constructing a function that simultaneously achieves specified double zeros in both spatial and frequency domains appeared analytically impossible under standard Fourier uncertainty principles.

Maryna Viazovska conquered this impossibility through an inspired synthesis of modular forms, quasimodular forms, and integral transforms. In her 2016 breakthrough, Viazovska constructed the magic function by expressing it as an integral of modular forms over the Poincaré upper half-plane (upper half-plane = {τ in complex numbers such that Im(τ) > 0}).

Viazovska utilized the classic Jacobi theta functions.

where q = e^{π i τ}, alongside the Eisenstein series (E_2(τ), E_4(τ), E_6(τ)). While E_4 and E_6 are true modular forms under the action of the modular group (SL(2, integers)), E_2 is a quasimodular form: its transformation law under τ mapsto -1/τ includes an anomalous derivative term.

Viazovska recognized that this anomalous transformation law was precisely what was needed to balance the Fourier transform! She defined an integral operator that integrates a carefully engineered modular form (psi(τ)) against a kernel function involving Bessel functions and Laplace transforms along a vertical contour in the upper half-plane. The modular symmetry of the integrand under the Fricke involution τ mapsto -1/τ guaranteed that the function was its own Fourier transform up to an exact sign change.

Through this modular engine, Viazovska proved that the function touched zero with exact double roots at the precise radial distances where lattice points sit. The sign conditions required by Cohn and Elkies were satisfied with flawless analytical perfection. In twenty-three crystalline pages, Viazovska demonstrated that the E₈ lattice is the absolute densest packing of spheres in eight dimensions. One week later, by adapting her modular forms to higher symmetries, she and her collaborators conquered the Leech lattice in twenty-four dimensions. Where Hales had required sixteen years, hundreds of thousands of lines of verification code, and server farms to settle three dimensions, Viazovska unleashed the pure, concentrated power of modern modular forms.

13. The Kissing Number Problem – Newton versus Gregory

The mathematics of sphere packing is intimately bound to a sister problem that ignited one of the most famous scientific disputes in seventeenth-century Britain: the Kissing Number Problem.

The kissing number tau_d is the maximum number of equal, non-overlapping spheres that can touch (or “kiss”) a central sphere of the same radius simultaneously. In two dimensions, the problem is trivial: exactly six pennies can touch a central penny on a flat table, forming a rigid hexagonal flower.

In three dimensions, the problem sparked an intense debate in May 1694 between Sir Isaac Newton and the Scottish mathematician and astronomer David Gregory. Newton asserted that the maximum kissing number in three dimensions was 12. Gregory argued that because the total surface area of a sphere is significantly larger than twelve spherical caps, there appeared to be enough residual solid angle to squeeze in a thirteenth sphere (tau_3 = 13).

The Newton-Gregory debate remained unresolved for more than two and a half centuries. The difficulty arose from the geometric “slack” in twelve-sphere configurations: when twelve spheres touch a central sphere in the face-centered cubic arrangement, they can be rolled and shifted continuously across the surface without colliding. Could these microscopic degrees of freedom be rearranged to accommodate a thirteenth sphere?

In 1953, Dutch mathematicians Kurt Schütte and Bartel Leendert van der Waerden finally proved that Newton was right: the maximum kissing number in three dimensions is strictly 12. In four dimensions, the kissing number remained open until 2003, when Oleg Musin proved that tau_4 = 24, achieved by the magnificent 24-cell regular polychoron.

Remarkably, the kissing number problem is known in only four dimensions across all of mathematics: dimension 1 (tau_1 = 2), dimension 2 (tau_2 = 6), dimension 3 (tau_3 = 12), dimension 4 (tau_4 = 24), dimension 8 (tau_8 = 240, achieved by the roots of E_8), and dimension 24 (tau_24 = 196,560, achieved by the minimal vectors of the Leech lattice). The exact solutions in dimensions 8 and 24 were discovered by Andrew Odlyzko and Neil Sloane in 1979 using Delsarte linear programming—foreshadowing the exact dimensions where Viazovska would solve sphere packing four decades later.

14. Rigorous Formal Interval Arithmetic in Theorem Provers

To appreciate how the Flyspeck Project achieved machine-certified certainty, one must examine the computational engine that certified Hales’s non-linear optimizations: formal interval arithmetic within the logical kernel of HOL Light.

In standard scientific computing, numerical calculations are performed using double-precision floating-point arithmetic compliant with the IEEE 754 standard. While floating-point hardware is blisteringly fast, it is inherently approximate: every arithmetic operation introduces microscopic rounding errors at the fifty-third bit of precision. In long chains of iterative non-linear optimization, these microscopic rounding errors can accumulate, drift, or flip conditional inequality branches, leading to catastrophic false-positive proofs.

To eliminate this hazard, Flyspeck implemented rigorous interval arithmetic inside the formal logic of HOL Light. In interval arithmetic, a real number x is represented not by an approximate float, but by a closed interval of rational numbers [x, x] such that x in [x, x]. When performing arithmetic operations, the endpoints are computed with rigorous outward rounding.

For transcendental functions—such as square roots, trigonometric functions, and multi-variable solid angle formulas—Alexey Solovyev and Thomas Hales formalized rigorous Taylor series expansions with explicit, machine-verified Lagrange remainder error bounds.

Crucially, in the Flyspeck architecture, these interval operations were not executed by an unverified external C++ program. Every interval calculation was executed as a formal deduction rule within the HOL Light kernel! Each inequality verified by the computer generated a formal logical certificate proving that the score function over a given polyhedral region was strictly bounded away from zero. By processing hundreds of thousands of interval boxes through the trusted kernel, Flyspeck guaranteed that no hardware fault, compiler optimization bug, or numerical round-off error could contaminate the final proof.

15. The Evolution of Mathematical Proof – From Four-Color to Flyspeck

The completion of Flyspeck represents the culmination of a half-century philosophical crisis regarding the nature of mathematical proof in the computer age. That crisis began in 1976, when Kenneth Appel and Wolfgang Haken of the University of Illinois announced the proof of the Four-Color Theorem—the assertion that every planar map can be colored using at most four colors such that no two adjacent regions share the same color.

Appel and Haken reduced the Four-Color Theorem to an unavoidable set of 1,936 reducible map configurations, which were checked by an IBM 370 mainframe computer over 1,200 hours of computation. The proof provoked widespread philosophical outrage within the mathematical establishment. Eminent mathematicians argued that a proof that could not be read, surveyed, and verified by a single human mind in its entirety did not qualify as mathematics. Was human understanding obsolete?

The doubts surrounding Appel and Haken’s proof persisted for three decades because human inspection of their computer code revealed minor bugs and missing cases that required subsequent patches. The ambiguity was only definitively resolved in 2005, when French computer scientist Georges Gonthier produced a fully formalized, machine-checked proof of the Four-Color Theorem inside the Coq proof assistant.

Seven years later, in 2012, Gonthier achieved an even more astonishing milestone: the formalization in Coq of the Feit-Thompson Odd Order Theorem—a foundational pillar of finite group theory whose original 1963 paper spanned 255 pages of dense, abstract algebra. Gonthier proved that pure, highly conceptual human mathematics could be formalized with total rigor.

The Flyspeck Project united these two streams: the massive, brute-force computational calculations of the Four-Color Theorem with the profound geometric theory of the Feit-Thompson proof. By proving that a 400-year-old open conjecture involving complex non-linear geometry, global optimization, and gigabytes of computational data could be completely verified down to first-order logic, Thomas Hales established the modern paradigm of machine-certified truth. Today, as automated reasoning and artificial intelligence systems begin generating novel mathematical conjectures, the formal proof assistants born from Flyspeck stand as the ultimate guardians of mathematical truth.

16. Universal Optimality – The Ground States of Matter

In 2019, Maryna Viazovska, together with Henry Cohn, Abhinav Kumar, Stephen D. Miller, and Danylo Radchenko, achieved a crowning synthesis that elevated the sphere packing problem into the fundamental physics of matter: the proof of universal optimality for the E_8 lattice and the Leech lattice.

Sphere packing is essentially the study of hard-sphere potentials: particles interact as infinitely rigid billiard balls that cannot overlap. But in the physical universe, atomic and subatomic particles interact through continuous force laws governed by potential energy functions—such as gravitational attraction, electrostatic Coulomb repulsion, Yukawa nuclear forces, and Gaussian core potentials.

In 2007, Henry Cohn and Abhinav Kumar formulated the concept of universal optimality. A configuration of particles is defined as universally optimal if it minimizes the total energy per particle among all possible arrangements of the same density, simultaneously across every natural potential energy law whose force decays smoothly and monotonically with distance.

This definition is audacious. Completely monotonic forces encompass a vast family of physical interactions: inverse-power decay laws (including Newtonian gravitation and electrostatic repulsion), exponential screening, and Gaussian potentials. To claim that a single geometric arrangement minimizes potential energy simultaneously under all such force laws is to assert that the configuration forms the universal ground state of matter in that dimension.

In a tour de force paper published in the Annals of Mathematics in 2022, Viazovska and her collaborators proved that the E_8 lattice in dimension 8 and the Leech lattice in dimension 24 are universally optimal! By extending Viazovska’s modular form magic functions to a continuous family of Laplace transforms, the team proved that no matter what repulsive potential governs the particles, nature will always freeze them into the crystalline perfection of E_8 or the Leech lattice at zero temperature. Universal optimality links discrete geometry directly to statistical mechanics, condensed matter physics, and the crystallization of solids.

17. Error-Correcting Codes, Cryptography, and Shannon Capacity

Beyond the aesthetic purity of higher-dimensional geometry, sphere packing possesses immense technological importance in modern telecommunications, digital signal processing, and cryptography. In 1948, Claude Shannon published “A Mathematical Theory of Communication,” founding the discipline of information theory.

Shannon demonstrated that transmitting digital data across a noisy continuous communication channel—such as radio waves, fiber-optic cables, or satellite links—is mathematically equivalent to packing high-dimensional spheres! In Shannon’s geometric formulation, a transmitted message is represented as a point (a code vector) in an n-dimensional Euclidean space real spacen, where n corresponds to the number of degrees of freedom (bandwidth multiplied by time). Random thermal noise in the channel perturbs the transmitted point, displacing it into a spherical “noise cloud” of radius σsquare root of n surrounding the true signal.

To ensure that the receiver can decode the message without error, the code vectors must be spaced sufficiently far apart so that their noise spheres do not overlap. The problem of maximizing the transmission rate of data across a noisy channel at maximum channel capacity (the Shannon limit) is precisely the problem of finding the densest possible sphere packing in high-dimensional Euclidean space!

The legendary Leech lattice Lambda_24 is the crown jewel of channel coding. Discovered by John Leech while investigating the binary Golay code G_24—an error-correcting code capable of correcting up to three bit errors per 24-bit word, famously used by NASA’s Voyager 1 and 2 spacecraft to transmit crystal-clear photographs of Jupiter and Saturn across billions of miles of space—the Leech lattice provides the densest known sphere packing in 24 dimensions. Modern high-speed DSL modems, wireless cellular networks, and deep-space communication protocols utilize lattice constellations derived directly from cross-sections of the Leech and Barnes-Wall lattices to approach the theoretical Shannon capacity.

Furthermore, in the twenty-first century, lattice geometry has become the bedrock of global cybersecurity. As quantum computing threatens to shatter classical public-key cryptography (such as RSA and elliptic curves) via Shor’s algorithm, the global cryptographic community has transitioned to Post-Quantum Cryptography (PQC). The new NIST post-quantum encryption standards—such as ML-KEM (Kyber) and ML-DSA (Dilithium)—are built entirely upon the mathematical difficulty of hard lattice problems in high dimensions, specifically the Shortest Vector Problem (SVP) and Learning With Errors (LWE). The very same geometric properties that make sphere packing intractable in arbitrary dimensions provide the cryptographic armor that protects the digital secrets of human civilization against quantum decryption.

18. Conclusion – The New Epistemology of Mathematics

The journey from Johannes Kepler’s snowflake to Thomas Hales’s Flyspeck Project and Maryna Viazovska’s modular magic represents a profound transformation in the epistemology of science. It traces the arc of how humanity defines and discovers truth.

When proofs become so vast, intricate, and computationally complex that they exceed the biological processing capacity of the human brain, traditional peer review reaches its structural breaking point. The Flyspeck Project proved that computer proof assistants are not mere curiosities, but the essential cognitive exoskeletons required for the future of mathematics. By wedding the boundless creativity of human intuition to the unflinching logical rigor of verified machine kernels, mathematics has entered a new golden age—one where four-hundred-year-old mysteries are solved forever, and truth is certified beyond the shadow of a doubt.

Today, the legacy of the Flyspeck Project reverberates across the frontiers of computer science and pure mathematics. What Thomas Hales and his collaborators demonstrated was not merely that an ancient conjecture could be laid to rest, but that the boundary between human mathematical intuition and machine verification is inherently porous and synergistic. In universities and research institutes worldwide, automated proof checkers, interactive theorem provers, and neural proof-synthesis engines are standardizing the formalization of mathematics. As humanity confronts ever more complex combinatorial systems, multi-dimensional manifolds, and planetary-scale optimization problems, the machine-certified certainty forged in the crucible of Flyspeck ensures that the mathematical foundations of our technological future remain unshakeable.