THE PROOF IN THE CODE

How the labor-intensive process of proving mathematical theorems was transformed by computational tools.

Journalist Hartnett examines how Lean, an open-source computer program for validating mathematical proofs, emerged from a small, loosely organized group of collaborators pressing mathematics toward new thinking. In 1998, mathematician Tom Hales solved the Kepler conjecture, a notoriously difficult problem articulated by Johannes Kepler in 1611. Hales’ solution relied on inventive computational techniques, but when submitted to a leading journal, reviewers—unfamiliar with such methods—took years before concluding they could not validate it. As Hartnett observes, some traditional mathematicians relied on covering “blackboards with rows of chalky equations, while others fill reams of scrap paper filled with attempts to find arguments that generate a proof,” distrusting machines to certify results. Familiarity with mathematical terms is helpful while Hartnett delivers a largely accessible account, invoking concepts such as formal proofs and interactive theorem provers (ITPs). Central figure Leo de Moura of Microsoft Research leads the development of Lean by a global community of volunteers. Colorful high-profile characters include mathematicians Terry Tao, Jeremy Avigad, Kevin Buzzard, and Peter Scholze. In one pivotal episode, Scholze, a traditionalist who tested proofs in his mind but—“due to the complexity of the proof, and how significantly he thought it could change mathematics, due to all the beer he had had the night before his final breakthrough”—asked whether Lean could verify the proof. Lean’s successful verification marked a turning point in the program’s acceptance, energizing collaborators to continue enlarging “the scope of mathematical knowledge that could be verified by machines.” Especially for math-curious readers, programmers, and those following AI trends, de Moura’s “truth machine” is a fascinating example of how cultural clashes and creativity can create new paradigms.

Proofs, personalities, and machines collide—intriguingly—at the uneasy intersection of mathematics and computer science.