Proof Positive: The Case for Investing in AI-Powered Math Tools

Tom Kalil

Proofs are the cornerstone of math, defining its quest for truth. Yet, in many ways, they are as much art as they are science. Finding proofs requires rigor, precision, and deep understanding. Often, a good proof reads like poetry, introducing completely new strategies and techniques and embodying elegance, beauty, and the care and passion mathematicians bring to their field.

However, proofs can have errors, and they are often hard to verify. Proofs are also getting exceedingly long and complex, which compounds these problems. Just recently, researchers at Imperial College London were trying to formalize the proof of Fermat’s Last Theorem. During this translation, a researcher discovered an error in a foundational 1965 proof by Norbert Roby, where a missing symbol rendered the original argument invalid.

How many other mistakes are lurking in decades-old – or even centuries-old – proofs? How can mathematicians shield future proofs from errors? Could an AI-powered proof “verifier” help find and correct them?

If so, the implications could be felt far beyond dusty math classrooms and elite universities. AI-proofing tools could help usher in a new era of internet safety, helping developers create foolproof, hack-proof code and improving security around financial transactions, to name just two real-world implications.

This is an area that deserves serious investment from both the public and private sectors. In addition to supporting researchers and developers with grants, funding, and tax incentives, government and industry must also robustly support educational programs that create open-source collections of theorems, proofs, and math problems to help benchmark the field.

The concept of mathematical proofs began with the ancient Greeks, who systematically used axioms and logic to prove geometric statements. They have become central to the field; they are the only way mathematicians can verify a theorem. Proofs tie together axioms, definitions, and theorems into a harmonious structure and establish relationships between disparate ideas, often revealing underlying unity.

Currently, AI can help check some proofs. But it lacks the ability to reason like a mathematician. Put differently, AI works great within known math frameworks, so it is less effective at exploring new areas where there’s little knowledge, structure, or data. Researchers are working to break through these barriers. Their goal is a day where AI can assist with and produce completely novel proofs at the frontier of math research and, in doing so, help uncover new mathematical knowledge.

It sounds esoteric and arcane, but the implications for society would be far-reaching. For example, such AI could help prove the theories that underlie technologies in physics, engineering, cryptography, and computer science, leading to safer products like self-driving cars and improved aviation controls.

Modern encryption methods rely on mathematical proofs to ensure security. An AI proof-checker could verify protocols and their implementations before they are exploited and accelerate the development of next-generation security measures, such as those resistant to quantum computing attacks.

To be sure, the field is years away from realizing this reality, but it’s getting closer every day. A new $9-million fund that our team helped launch with the support of the algorithmic trading firm XTX will help the development of these new AI tools.

And this is just the start. The transformative potential of AI-powered proof-checkers demands serious investment. The public and private sectors must collaborate to fund research, support educational STEM programs, and incentivize innovation. By doing so, we ensure that mathematics continues to serve as the foundation for safer, more efficient, and groundbreaking technologies.

Tom Kalil is the CEO of Renaissance Philanthropy.