Math long resisted a digital disruption. AI is poised to change that
Modern formalization, supercharged by AI, could radically change the way people do mathematics
Mathematician Kevin Buzzard of Imperial College London is training computers how to prove one of the most famous problems in math history: Fermat’s last theorem.
Resolving the problem isn’t the point. There’s already an accepted proof that was finalized in 1998. That work is a tortuous maze of mathematics that fills about 130 pages over two papers. It spans mathematical fields and unites abstract ideas that previously seemed to have little to say to one another. To know the proof is to know a wide swath of mathematics. In the future, Buzzard says, a computer program that can verify something so sprawling will be able to help mathematicians find, scrutinize and solve a wide range of problems.
For years, Buzzard and a handful of mathematicians have been working on projects like this to formalize mathematics. Historically, formalization has involved expressing mathematical ideas as precisely as possible, erasing all ambiguity. Today, that means translating definitions and theorems into computer code so that a specialized program can verify every painstaking step.
Formalization “is a new paradigm for mathematical proof writing that essentially demands the proof writer be way more rigorous than usual,” says mathematician Emily Riehl of Johns Hopkins University. “The computer is not really filling in the details.” The person who is writing the proof has to do that instead.
But formalizing the proof of Fermat’s last theorem is just the cornerstone of an even larger vision: to build a digital library of all of mathematics that will enable computers to be useful assistants to mathematicians.