[FOM] What is the current state of the research about proving FLT?]

[Colin McLarty]

Re Harvey's questions:

There are many new advances and alternatives in proving FLT since Wiles.
Most notably Mark Kisin in 2009 and 2010 gave two new proofs of Modularity
at once simplifying and generalizing the Modularity Thesis beyond
Taylor-Wiles.  These do not much change the basic tools (or the logical
assumptions).  And the proof of FLT remains inaccessible to, say, the
average PhD number theorist.  Here are two measures of how the basics
remain as Wiles gave them:

1) The standard expositions preparing a PhD number theorist to work on the
proofs of FLT are still based on the Wiles proof.  Both are several hundred
pages long and neither gives a complete proof. They are
Cornell-Silverman-Stevens, *Modular Forms and Fermat's Last Theorem*, and
Takeshi Saito* Fermat's Last Theorem.*

2) In 2016 Matthew Emerton's fifth year PhD student Drew Moore arranged a
one quarter graduate seminar at Chicago with the goal "to prove Fermat's
Last Theorem (with some black boxes)."   That seminar was based on the
Cornell-Stevens-Silverman book.  See
http://math.uchicago.edu/~drewmoore/FLTWinter16/index.html

If something new broke i 2017 then I do not know it yet.  I expect some day
graduate number theory textbooks will prove FLT in a chapter, but that will
depend on very great substantial new insights in number theory (such as are
already occurring), not just on logic or exposition.

Re Joe Shipman:

The problem with McLarty’s results is they still do not amount to a simple
> metatheorem which can be applied to the STATEMENT of a result, because
> ZFC+UA is not conservative over ZFC even for pi^0_1 statements. Rather,
> McLarty analyzes the entire edifice build by Grothendieck and his followers
> and identifies some specific lemmas which suffice for Wiles and which can
> be proven without UA.


I do much more than that.  I identify all theorems in the EGA and SGA that
are not obviously provable in PA, and show that the very proofs of them
which are already given in the EGA and SGA can be formalized in a
conservative extension of Finite Order Arithmetic.  One proof at the base
of all of those required substantial revision.  It is used throughout the
EGA and SGA but is actually in Grothendieck's 1957 Tohoku paper on
cohomology, namely the proof that  module categorie have "enough
injectives."

As to the other end of the proofs of FLT, I will give results at the 2018
ASL North American Annual Meeting of the ASL, in Macomb, Illinois, on
taking classical results in class field theory (overtly second order
arithmetic) and proving them in EFA.

Colin
 .


On Sun, Jan 7, 2018 at 4:34 AM, Harvey Friedman <hmflogic at gmail.com> wrote:

> From Arnon Avron, 1/6/18
>
> > Let me say it with even stronger words: in my opinion,
> > a theorem can *really* be considered
> > as proved in mathematics only when it reaches the stage in which its
> original
> > proof has been  sufficiently simplified,  and then presented in textbooks
> > in a way that most of the mathematicians can read and verify for
> themselves.
> > If this cannot be done  or is not going to be done, then something
> > very suspicious is going on.
>
> Readers may want to look at
> https://www.scientificamerican.com/article/are-mathematicians-finall/
>
> Also, I was under the impression that there are now some alternative
> proofs of FLT around, and if so, I wonder what the situation is with
> the axiomatic issues. Perhaps I am confusing this with Mordell's
> Conjecture. By the way, what is the logical status of the proofs of
> that? Perhaps Colin can comment on these questions.
>
> Harvey Friedman
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180108/0a71aa56/attachment.html>