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 uses the Lean theorem prover to formalize and verify the proof.

Buzzard stated that a computer program that can verify the proof will help mathematicians find, scrutinize and solve a wide range of problems. ’s Engineering and Physical Sciences Research Council. 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 2024, the formalization effort reached a milestone by proving that a certain thing was finite. Buzzard targeted a five-year timeline to finish the project. Many of Buzzard’s colleagues at Imperial College London are exploring ideas used in the proof of Fermat’s last theorem.

Formalization as a Tool for Mathematical Verification Formalization 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 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.

History and Proof of Fermat’s Last Theorem 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.

AI and Historical Efforts 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 2024. In February 2024, Maryna Viazovska and others finished formalizing proofs of the Kepler conjecture in eight and 24 dimensions by combining AI with an interactive theorem prover. Maryna Viazovska, a Ukrainian mathematician, earned a Fields Medal in 2022 for work related to the proofs.

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, Thomas 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.

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.