AI Checked a Fields Medal-Winning Proof in Five Days

The sphere-packing story reveals why checking a theorem and building mathematics that others can reuse are different achievements.

Five days is the number that attracts attention.

According to the researchers’ account, that was how long Gauss, an AI system developed by Math, Inc., took to complete the remaining formal proofs needed for a major theorem about packing spheres in eight dimensions. It worked from an existing mathematical blueprint and a substantial body of human-written Lean code. [1]

The result was a complete proof checked by Lean’s logical kernel. Yet the researchers continued working.

There is no contradiction here. Their project had several goals, and reaching the final theorem fulfilled only part of them. They also wanted a development that mathematicians could read, maintain and use to prove something else. [1]

To understand why that matters, it helps to begin with the original mathematics.

Imagine stacking identical oranges. Gaps remain between them, however carefully you arrange the pile. The sphere-packing problem asks how much of space identical, nonoverlapping balls can occupy.

Now replace the three coordinates used to locate an orange with eight coordinates. We cannot visualize…