The Proof in the Code
Kevin Hartnett
Quanta Books, $30
In 2024, the International Mathematical Olympiad had an unusual entrant. Google Deepmind had set AlphaProof, a newly trained AI program on that year’s competition questions, although as an unofficial participant. In the contest, top math students from across the world solve six advanced math problems over two days. AlphaProof made headlines and the silver-medal level cutoff by scoring 28 points out of 42.
AlphaProof is a mathematical theorem solver, a system for proving mathematical statements. Just four years prior, training AI systems to automate mathematical reasoning had been a grand challenge. But Google Deepmind and other groups hoped that their efforts would equip AI systems with broader reasoning skills that could someday be applied to real world problems, using logic to potentially free AI tools of hallucinations, instances of made-up information.
Many of these programs owe their success to the proof assistant program Lean. Leo de Moura launched Lean as a tool for checking software code in 2013 when he was a software engineer at Microsoft Research. But today, mathematicians and AI researchers are Lean’s biggest cheerleaders. In his new book The Proof in the Code, journalist Kevin Hartnett traces that evolution.
Hartnett chronicles de Moura’s persistence in developing software that had no immediate commercial benefit and the dogged determination of a small group of mathematicians who persuaded their field to embrace the program. Throughout the book, Hartnett introduces a host of characters from around the world who saw in Lean a new way to assess mathematical truths and played roles big and small in making Lean more user-friendly. Taken together, this makes for an inspiring story of collaboration.
In the initial chapters, Hartnett sprinkles in explanations about the similarities between math and coding that demonstrate how Lean’s use could so naturally be transplanted to research math. “Both are written in exact syntax as a series of logical steps, each one leading to the next,” Hartnett writes. “A gap in the logic of a proof is like a bug in software code.” A program runs when the code has the correct logic. A new math theorem is the result of a correctly written proof.
Almost immediately after Lean’s launch, Jeremy Avigad of Carnegie Mellon University began setting it up to write math proofs. Lean and other proof assistant programs, also known as interactive theorem provers, can verify new human-written mathematical proofs, which sometimes span hundreds of pages and can take months to review. The programs can’t come up with new proofs, but by helping to ensure that proofs are error-free, they can allow mathematicians to establish new mathematical facts faster for use in newer proofs. Still, proof assistants were clunky pieces of software that required writing math in an entirely different way.
To work with proof assistants, mathematicians had to translate problems from plain language into code and create libraries of coded definitions and theorems of basic math concepts. For instance, when Kevin Buzzard, a math professor at Imperial College London, was writing up problem sets to teach his undergraduate students to work with Lean, he quickly ran into an unexpected hurdle. “Lean asked him to prove that 2 is not equal to 1,” Harnett writes. “It’s a statement so clearly true that human beings, in normal conversation, wouldn’t waste a moment justifying it.” But Lean required him to prove inequality before using it.
For a long time, there just wasn’t enough math in Lean’s libraries for it to be useful to mathematicians. And more math couldn’t be coded without more mathematicians using the program. Hartnett shares what it took for some mathematicians to popularize Lean. For instance, in 2018, Buzzard and others set about translating perfectoid spaces into Lean. Coding this sparkly new innovation in arithmetic geometry took them months of work and many thousands of lines of code. And these efforts worked. By 2025, “tens of thousands of users across academia and technology were launching increasingly ambitious projects on top of Lean,” Hartnett writes. This included AI researchers, who had found in Lean in an extensive library of advanced math required to train math-solving AI models such as AlphaProof.
Both de Moura and the mathematicians wanted to build a truth machine, “a computer program that can provide a complete, 100 percent guarantee that a chain of logic is correct,” Hartnett writes. While for de Moura, the truth he was after was to know for sure that the code for computer programs, like Microsoft Word, was correct and bug-free, for mathematicians, a truth machine could make mathematical proof discoveries more rigorous, organized and exact.
In tracing this history, The Proof in the Code jumps between timelines, introducing characters and anecdotes without always clearly stating their importance. This can be confusing for readers, but for the mathematically curious, the book adds an engrossing texture to the story of Lean and its place in a new, recent chapter in the story of math.
Buy The Proof in the Code from Bookshop.org. Science News is a Bookshop.org affiliate and will earn a commission on purchases made from links in this article.
Read the full article here
