The four-color theorem states that any map can be colored with four colors in such a way that adjacent countries do not receive the same color. This theorem is one of the most famous math problems ever to be solved by computer. Last year, Georges Gonthier gave a completely formal proof of the four-color theorem. This means that every step of the proof has now been carefully checked all the way down to the fundamental axioms of mathematics. I will describe Gonthier's project and explain how it relates to my current work on packing spheres.