Fermat's Last Theorem

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 )

   1. Lean4 proofs are available at https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/NumberTheory/FLT

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 elliptic curves. (Note that elliptic curves are not defined yet).

3. See notes from Steven Nguyen et al 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.

   1. Current status of this project: Definition of projective curve (because elliptic curves are projective curves)

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 and Richard Taylor are leading a project to formalize Fermat's Last Theorem in Lean. This is being done as an open source project: for more details see Fermat's Last Theorem and A Blueprint for Fermat’s Last Theorem.