The Proof Is in the Code

In the last decade, proof assistants have revolutionized how mathematicians establish whether a mathematical theory is valid. One in particular, called Lean, has risen to the forefront of the field. Its productivity-enhancing capabilities are behind several notable proofs that have been demonstrated in recent years. What’s more, its integration with Artificial Intelligence technologies is contributing to a rapid pace of new advances in solving long standing but, until this year, unproven mathematical conjectures.

Much of that story is now being told in Kevin Hartnett’s The Proof in the Code: How a Truth Machine Is Transforming Math and AI, which is proving to be an exceptionally well-timed book. It captures the short history of the rapid development of the Lean proof assistant, which is contributing to a revolution in how mathematicians do what they do. Hartnett’s book is all the more remarkable because it doesn’t require readers to have an extensive background in either mathematics or computer science to both follow the story and understand its significance.

And what a significant story it is. Here’s a short summary of how Lean is aiding the advancement of mathematics:

• It can automate large parts of the process of verifying mathematical proofs.
• Its results are trustworthy. If a proof is validated in Lean, the proof will hold.
• Its library allows mathematicians to take advantage of proofs developed by their peers, using them as modular building blocks to help establish new proofs.
• It can handle very sophisticated proofs developed by the world’s top mathematicians.
• It facilitates massive collaboration efforts among mathematicians and other contributors.
• It can be integrated with Artificial Intelligence (AI) technologies, such as reinforced learning techniques and Large Language Models, which can both improve its performance and the performance of the AI systems.

All of these things underscore the role of Lean as an amazing productivity enhancing software tool for its users. But it wasn’t always that way. Perhaps even more remarkably, Lean didn’t start out as a tool aimed at helping mathematicians.

As originally envisioned by Leo De Moura, who wrote several generations of its code, it was supposed to be a tool to help software developers find and fix bugs before they released software. A chance discussion with mathematician Jeremy Avigad in 2013 identified the potential of the code to aid mathematicians in developing their proofs, which ultimately set the direction of Lean in motion.

The rest of Harnett’s story is how their efforts pulled in other key players who recognized its potential and worked through its development challenges to make it useful first, then to make it more and more capable.

For a story that involves many mathematicians and the math they were seeking to validate, Harnett keeps mathematical equations and symbols to a minimum. That’s a vital requirement in making the story accessible to a general audience and showcases Hartnett’s experience as a math writer. It’s not until the later chapters of the book that mathematical statements begin appearing in the text, which are backed by plain language descriptions, which makes them very approachable.

Even more remarkably, the only example of Lean code that Hartnett presents is contained in the book’s Appendix. The example is Lean’s version of a 2,300+ year-old proof by Euclid that confirms there is always another larger prime number, which is to say that prime numbers extend into infinity.

If you only read one math book this year, this is the one to read. It’s a fantastic introduction to some of the most advanced happenings going on in the world of maths and computer science and what is becoming possible today that hasn’t been before. Highly recommended!

If you’re interested in more discussion, Hartnett was recently interviewed by Breaking Math‘s Autumn Phaneuf and Noah Giansiracusa. Here’s the video of the interview: