Mathematician Kevin Buzzard Trains Computers to Prove Fermat’s Last Theorem

# Mathematician Kevin Buzzard Trains Computers to Prove Fermat’s Last Theorem LONDON (Substrate) -- Kevin Buzzard, a mathematician at Imperial College London, is training computers to prove Fermat’s last theorem. The theorem, which has an accepted proof finalized in 1998, fills about 130 pages over two papers. Buzzard’s project formalizes and verifies the proof using Lean.

Buzzard stated that a computer program that can verify the proof will help mathematicians find, scrutinize and solve a wide range of problems. In 2023, with support from the U.K.’s Engineering and Physical Sciences Research Council, Buzzard launched his formalization project with Fermat’s last theorem.

About 30 people were contributing to the effort by writing code for Lean at first, and just over 60 people have had their coded contributions verified and accepted in the project.

In January, the formalization effort reached one of its first major milestones. “We proved that a certain thing was finite,” paving the way for the next step, Buzzard says. The effort required for that milestone, however, has led him to doubt whether they’ll finish in his targeted timeline of five years.

Many of Buzzard’s colleagues at Imperial College London are exploring ideas used in the proof of Fermat’s last theorem.

translates definitions and theorems into computer code for verification by a specialized program.

Kevin Buzzard and a handful of mathematicians have been working on projects to formalize mathematics for years. Buzzard’s journey with formalization began in 2017, when he reviewed a paper for publication in a math journal and had a lengthy exchange with the paper’s author. During a talk in September, Buzzard stated that he got quite unhappy with the state of things in mathematics.

Formalizing the proof of Fermat’s last theorem is the cornerstone of a vision to build a digital library of all of mathematics. Modern formalization has been a niche effort because it requires expressing mathematical ideas as code. Emily Riehl, a mathematician at Johns Hopkins University, stated that formalization is a new paradigm for mathematical proof writing that essentially demands the proof writer be way more rigorous than usual.

In a separate project funded by Renaissance Philanthropy, Kevin Buzzard and Rutgers mathematician Alex Kontorovich are formalizing problems from a list of recent thorny theorems. Riehl stated that a theorem prover with access to a robust library could be used to identify hallucinations and other mistakes in mathematical proofs, and that’s game changing.

In or around 1637, Pierre de Fermat scribbled a problem and a note in a copy of Arithmetica by Diophantus, a book by third-century Greek mathematician Diophantus.

Fermat’s last theorem involves the equation an + bn = cn. Fermat stated that there are no whole numbers for a, b and c that solve the equation if n is greater than 2. Fermat’s son discovered the book and the note after his father’s death.

British mathematician Andrew Wiles cracked Fermat’s last theorem in the late 20th century and collaborated with mathematician Richard Taylor to finalize the proof. In 1847, German mathematician Ernst Kummer proved that Fermat’s last theorem held for the regular primes and developed ideas that laid the groundwork for algebraic number theory.

in Computer-Assisted Proofs Artificial intelligence has propelled efforts to combine large language models with theorem provers for autoformalization.

Efforts to combine large language models with theorem provers are spearheaded by technology companies. Lean first appeared in 2013; it is a programming language and an interactive theorem prover. Leo de Moura, a computer scientist at Microsoft, designed Lean as a way to verify mathematical arguments, especially in computer code.

Lean is the theorem prover used to formalize Maryna Viazovska’s proof in February. In February, by combining AI with an interactive theorem prover, Ukrainian mathematician Maryna Viazovska and others finished formalizing proofs of the Kepler conjecture in eight and 24 dimensions — digital versions of work that had earned Viazovska a Fields Medal in 2022.

The Kepler conjecture is a statement about the optimal way to stack spheres originally posed by Johannes Kepler in the 17th century. In 1998, Thomas Hales announced that he and his student Samuel Ferguson had used a computer to prove the Kepler conjecture. From 2003 to 2014, Hales used digital assistants to formalize and verify his proof of the Kepler conjecture.

Some mathematicians have used interactive theorem provers in the last few decades to verify existing mathematical proofs. In 1956, researchers at the RAND corporation introduced a computer program called a logic theory machine, which checked proofs published in Principia Mathematica. Principia Mathematica is a landmark series of books by mathematicians Bertrand Russell and Alfred North Whitehead.

Herbert Simon was one of the researchers behind the logic theory machine. Bertrand Russell wrote in a letter to Herbert Simon that he was delighted to know that Principia Mathematica can now be done by machinery. Bertrand Russell wrote in a letter to Herbert Simon that he wished Whitehead and he had known of this possibility before they both wasted 10 years doing it by hand.

“We’re really at the cusp of a change,” says Patrick Shafto, a mathematician and computer scientist at Rutgers University in Newark, N.J., and at DARPA, a research and development agency within the U.S. Department of Defense. Shafto stated that mathematics is now basically practiced at a board, as it was 100 years ago.

Shafto stated that in five years, it is very likely that every single young mathematician uses AI.