The Proof in the Code: How a Truth Machine Is Transforming Math and AI

Journalist Hartnett debuts with a thrilling account of “how one man’s quest to build a truth machine—a computer program that can provide a complete, 100 percent guarantee that a chain of logic is correct—is transforming the field of mathematics.” The program, called Lean, was developed in 2013 by Leo de Moura, a computer scientist at Microsoft who was trying to find a way to ensure that the computer code responsible for running programs like Word and Windows didn’t contain bugs or security weaknesses. Mathematicians adopted and expanded de Moura’s work, enabling the program to check complex mathematical proofs that were so intricate they were unlikely to ever be reasonably assessed by humans. In recent years, tech firms like Google DeepMind and Meta AI have used the program to train the next generation of artificial intelligence systems, reducing hallucinations and improving accuracy. In Hartnett’s capable hands, what might be a dry, technical report comes alive, as he explains in entertaining, accessible detail how linking AI and Lean enabled a DeepMind AI model called AlphaProof to perform at the level of a silver medalist at the International Math Olympiad in 2024 and how Lean may eventually be able to help AI systems tackle real-world problems outside the realm of mathematics. Readers will be captivated. (June)