Fermat's Last Theorem

As of 2022, a proof of Fermat's Last Theorem has not been proved in any 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, which is an essential component in the proof of Fermat's Last Theorem.