Communications of the ACM
Pushing the Frontiers of Mathematical Research
Efforts to verify a complex mathematical proof using computers have been successful.
Credit: Fadel Senna/AFP/Getty
For decades, mathematicians have turned to computers for help with tasks like big numerical calculations and visualizing complex geometric objects. Like a blackboard, the computer has been a handy tool that picks up where human capacity to juggle numbers, symbols, and pictures drops off.
Today, however, computers are playing an entirely new role: they are learning modern mathematics.
A loose-knit international group is using computer proof assistants, originally developed to check formal software correctness, to create online libraries of mathematical theorems and proofs. The theorems housed in these libraries can then be called upon as building blocks for proofs of new mathematical results. The hope is that the libraries one day will encompass the entirety of mathematical knowledge.
"It's a completely new way to do mathematics that is very satisfying," said mathematician Kevin Buzzard of the U.K.'s Imperial College London.
Buzzard discussed this work in one of the most-watched lectures at the 2022 International Congress of Mathematicians in July this year. (The Congress, originally scheduled to be held in Saint Petersburg, Russia, was transformed into an entirely online event after that country's invasion of Ukraine.) Around the same time, a paper appeared on the arXiv containing what might be called a "proof assistant manifesto," laying out progress achieved and describing challenges ahead. Buzzard is one of the paper's 10 authors, along with ACM A.M. Turing Award recipient Leslie Lamport.
During the course of his career in number theory and algebraic geometry, Buzzard has worked on pure mathematics with no obvious applications. He describes his latest work with computer proof assistants as also "100% blue-sky research," explaining, "It's interesting, important, and beautiful. But I can't see the future. I don't know what killer app might come out of this work."
Verifying Proofs Down to the Axioms
Computer proof assistants, also called interactive theorem provers, began to have a significant impact in mathematics starting with the work of Thomas Hales of the University of Pittsburgh. In the late 1990s, Hales announced a solution to a venerable sphere-packing problem called the Kepler conjecture. While his approach was generally accepted as correct, Hales' use of a computer program to sort through a huge number of possible packings left many skeptical.
Hales then embarked on a multi-year project to validate his solution by recasting it as a "formal proof," a thoroughgoing version of the proof in which every logical inference is checked, down to the fundamental axioms of mathematics. Formal proofs, far too verbose and tedious for humans to read, are tailor-made for computer proof assistants. In 2014, Hales and 20 collaborators completed a computer verification of the Kepler proof.
In parallel with this work, during the early 2000s, a few mathematicians began to use proof assistants to formalize proofs of several classic mathematical results. The work was slow and painstaking, and the technology rather off-putting. As a result, formal proofs remained something of a niche area, far from the frontier of mathematics.
Buzzard got into the act after listening to a 2017 lecture in which Hales described his experiences using proof assistants. "That lecture changed my life," said Buzzard, as he realized that proof assistants could handle the theorems that mathematicians are working on at the frontier of research today. "Computer scientists were figuring out how to write the software, to make it useful," Buzzard said. "They've done that now. Now it's our turn."
The True Value of Proof Assistants
As the name suggests, a computer proof assistant is very good at verifying proofs, but its true value in mathematics lies elsewhere, in its ability to store mathematical results and the fundamental logic supporting them. Every theorem, lemma, and proposition that was used or proved in the course of verifying, for example, Hales's solution of the Kepler conjecture, now sits in the memory of a proof assistant, ready to be called upon as raw material to build proofs of new theorems.
When Buzzard was lured into the area by the thought of a vast online library of mathematical results, initially he was shocked to find that the mathematical knowledge that had been formalized had enormous gaps. "There was stuff that Gauss knew that the theorem provers didn't know," he said, referring to the 18th century mathematician and physicist.
So Buzzard set a bunch of undergraduate students to work formalizing all of the theorems and proofs found in a typical undergraduate mathematics major, using a proof assistant called Lean. The students were enthusiastic about learning mathematics in this new way and became adept at using Lean.
The process also brought new perspectives. "Some bits of mathematics operate close to the axioms," Buzzard observed. For example, many humans find commutative ring theory, which is based on 10 axioms, to be quite abstract, but Lean "learned" it with ease, he said. Other parts of mathematics that are far more intuitive, like real numbers, proved to be much harder to program into Lean.
In 2020, as the project to formalize undergraduate mathematics chugged along, Lean was posed a new challenge. Peter Scholze of Germany's University of Bonn, a 2018 Fields Medal recipient and one of the most outstanding mathematicians of our time, was working on a new theorem with Dustin Clausen of Denmark's University of Copenhagen. Scholze posed a challenge: could Lean verify the theorem? This was no undergraduate fare, but mathematics at the cutting edge of research in algebraic geometry, a formidably abstract and technical area.
Johan Commelin, a postdoctoral student at Germany's University of Freiburg and an active member of the Lean community, assembled a team (including Buzzard) to try to meet the challenge. They began teaching Lean the entire background needed to prove the theorem. Commelin would describe chunks of the proof on an online discussion board used by the Lean community; volunteers would take up those chunks that fit their expertise and code them into Lean. Scholze was on hand to answer their mathematical questions.
After six months, a key lemma had been verified. In a blog post, Scholze excitedly reported that it was exactly that lemma that had raised doubts and led him to ask for verification of the theorem. He was enthusiastic to find that it is now possible to feed a research paper step by step into a proof assistant until the whole paper has been verified. "I think this is a landmark achievement," he wrote.
Verifying the lemma was a big achievement, but it still took another year to get the entire Clausen-Scholze theorem into Lean. Entering Lean code is time-consuming, so the volunteers searched for efficiencies wherever they could. As a result, Commelin was able to home in on exactly the properties required by a certain highly complicated object that appeared in the proof. This allowed him to make a contribution to the mathematics: he found a different, less-complicated object that would do the same job. The verification of the theorem was completed in July 2022.
This work showed, for the first time, that Lean could handle the full complexity of today's mathematical research. Efforts are currently afoot to formalize other similarly sophisticated results of modern mathematics. One is a formal proof of Fermat's Last Theorem, a landmark result that is extremely simple to state but whose proof relies on an enormous range of deep results from 20th century mathematics.
"Of course, we are not worried about whether the proof of Fermat's Last Theorem is wrong," Buzzard said. "We want to build the library. We want to make an extensive library that's capable of understanding what we are talking about" at the forefront of mathematics research.
A Gigantic Collaboration
The past few years have seen great progress, as hundreds of students and researchers have jumped into the work of building the library. As expertise grows, the process of entering mathematical results into proof assistants has sped up. Buzzard recounted the case of a recent combinatorics result by Thomas F. Bloom of the U.K.'s University of Oxford, completed and submitted for publication in December 2021. Bloom teamed up with Bhavik Mehta, a Cambridge University Ph.D. student and Lean expert, to verify the proof. Six months later, the journal's referees had still not passed muster on the proof, said Buzzard, "but the computer had checked absolutely everything, down to the axioms of mathematics."
Many of the results formalized in proof assistants have a number-theoretic and algebraic slant, reflecting the interests of the group of mathematicians who have contributed to building the library. A result with a very different, highly geometric flavor is the subject of a new formalization effort: Stephen Smale's mind-bending proof that a sphere can be turned inside out without tearing or creasing. Capturing this highly conceptual proof in a proof assistant will make available a whole new range of results from geometry and topology.
People following their own interests, filling in bits they believe are needed, challenging the limits of the software: this is how the library is being built. Some use Lean, others use different proof assistants such as Isabelle/HOL or Coq. There is no leader and no exact plan of where the work is headed. "It's a gigantic collaborative project being designed by hundreds of people," Buzzard said. "It's growing in a slightly out of control and very exciting way."
He noted that no one could have predicted that the digitization of music would lead to platforms like Napster and Spotify, which allowed musicians to connect with their audiences in entirely new ways. "We are digitizing mathematics," Buzzard said. "I am not entirely sure what's going to happen, but I do think it will inevitably change mathematics."
Allyn Jackson is a journalist specializing in science and mathematics, who is based in Germany.
No entries found