Look at the oranges in a fruit shop. They are often stacked in a neat pyramid. In 1611, Johannes Kepler said this is the best way to pack balls of the same size. About 74 percent of the space is filled.

A mathematician named Thomas Hales showed a proof in 1998. It was very long and used computers. Other experts could not be fully sure about it. In 2014, a computer program checked every step.

When Thomas Hales announced his proof of the Kepler conjecture in 1998, it came with hundreds of pages of arguments and a huge amount of computer work. The famous journal Annals of Mathematics asked a team of experts to check it. After years of work, the chief referee said he was 99 percent sure the proof was correct, but the referees could not check every computer calculation.

The paper was published in 2005. Hales was not happy with 99 percent. In 2003 he started a project called Flyspeck to rewrite the whole proof in a form that special software could check step by step. With more than twenty co-authors, he finished the project in August 2014.

A formal proof is written so that a program called a proof assistant can check each logical step, down to the basic rules of logic. Flyspeck used two such systems, HOL Light and Isabelle, and some of the heaviest numerical checks ran on cloud computers. This approach answers an old complaint.

When the four color theorem was proved with computer help in 1976, the philosopher Thomas Tymoczko argued that accepting a proof no human can read brings something like experimental evidence into mathematics. Formal proof has weak points, though. The software might contain a bug, and the formal statement of the theorem might not mean exactly what mathematicians intended. Supporters reply that the trusted core of HOL Light is small enough for people to inspect line by line.

The rewriting also paid off. A 2010 paper by Hales and colleagues listed errors in the original proof that had slipped past review. Most were small, and one gap needed a new argument, yet the result stood. Higher dimensions tell a different story. In 2016, Maryna Viazovska solved the packing problem in eight dimensions with a short proof that people can follow, work that led to a Fields Medal in 2022.