Towards formalization of Fermat's Last Theorem

[Timothy Y. Chow]

Freek Wiedijk wrote:

> Formalization of a proof of Fermat's Last Theorem is one of the Grand 
> Challenges of formalization of mathematics.  We are considering what is 
> the best way to get started on this. In particular we currently created 
> a project for this, see
>
>  https://www.cs.ru.nl/~freek/fltfps/
>
> The idea of this project is _not_ to start by formalizing proofs, but 
> first to formalize _definitions_ and high level _statements,_ both to 
> show the mathematical communicty what formalized mathematics looks like, 
> and to create a road map for a full formalization.  The approach is 
> similar to the one of Tom Hales' Formal Abstracts project.
>
> My question: does this sound reasonable, or will a different approach be 
> better?

I don't have an answer to your question, but I do have a comment.  I 
believe that this project will attract wider interest if, at the end, you 
are able to answer the question, what are the weakest axioms needed to 
prove Fermat's Last Theorem?

For example, it is a frequently asked question whether Fermat's Last 
Theorem is provable in PA.  This question is addressed, for example, in 
Angus Macintyre's appendix to Chapter 1, "The Impact of Gödel's 
Incompleteness Theorems on Mathematics, of the book "Kurt Gödel and the 
Foundations of Mathematics: Horizons of Truth" (Cambridge University 
Press, 2011).  I happen to think that this question is often asked with 
slightly misguided presuppositions; the asker is usually trying to ask if 
there is an "elementary" proof of FLT.  Macintyre's sketch, which in 
essence tries to replace all the fancy mathematical machinery in the proof 
with "finite approximations," addresses the literal question of whether 
FLT is provable in PA, but is also not what the "mathematician in the 
street" would think of as an "elementary proof."  Be that as it may, the 
question of which axioms are really needed to prove FLT continues to 
fascinate many people, so if you are able to give a definitive answer, I'm 
sure there would be a lot of interest.

Tim