Skip to content

Fermat's Last Theorem

Jump to bottom Edit New page
Jim Kingdon edited this page Oct 4, 2023 · 12 revisions

As of 2022, a proof of Fermat's Last Theorem has not been proved in any formal proof system. Here is a list of some of what has been written about this or things we can do:

  1. One piece of low hanging fruit is to add metamath proofs for the n=3 and n=4 cases. Proofs have been known for several centuries so there should be a wealth of published proofs to draw on. Also, these are needed because the proof of Fermat's Last Theorem via the Modularity Theorem does not include these two cases (reference: David Crisp's message to the metamath mailing list of 20 Feb 2023, https://groups.google.com/g/metamath/c/rJ5pHKbGSZg/m/sq6itfKSAwAJ )

  2. Another (apparently low hanging fruit) idea would be to prove the equivalences at https://en.wikipedia.org/wiki/Fermat's_Last_Theorem#Equivalent_statements_of_the_theorem which for one thing covers the connection to elliptical curves.

  3. See notes from Steven Nguyen at https://docs.google.com/document/d/19dXkojJJt6gq9rYLo6zbz7HpHpD9iMJJkY0LEpGqPs0/edit?usp=sharing which lists some of the pieces to using the Modularity Theorem to prove Fermat's Last Theorem. This includes some notes on mapping various concepts to (existing or proposed) metamath notation.

  4. Formalizing Norm Extensions and Applications to Number Theory, Maria Ines de Frutos Fernandez, Imperial College London, Machine Assisted Proofs, February 13 - 17, 2023, http://www.ipam.ucla.edu/abstract/?tid=19347&pcode=MAP2023 is about formalizing Local Class Field Theory (in Lean 3), which according to the abstract is an essential component in the proof of Fermat's Last Theorem.

  5. There is a formalization in Lean for the case where the exponent is a regular prime. Alex J. Best, Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi (2023), "Fermat's Last Theorem for regular primes", https://arxiv.org/abs/2305.08955

  6. Kevin Buzzard has an EPSRC research grant to spend 5 years of [his] life formalising Fermat's Last Theorem! The grant starts in October 2024 and the first aim is to reduce the problem to theorems which were known in the 1980s. See https://mathstodon.xyz/@highergeometer/111169967335367270 . This will be in Lean amd run as an open source project: https://mathstodon.xyz/@xenaproject/111170563403967905

Add a custom footer
Add a custom sidebar
Clone this wiki locally