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

[Joe Shipman]

Arnon, this is a little bit scandalous, but not a lot scandalous. The top people in the field were well aware that the “Universes” axiom could be eliminated in many cases including Wiles’s proof, but there “knowledge” of this fact merely amounted to “moral certainty” because NO ONE HAD EVER PUBLISHED A RELEVANT METATHEOREM.

They knew it could be done in the same way that they knew that the proof could be completely formalized in ZFC+UniversesAxiom in a computer-checkable way, and they regarded that project as also not worth their time.

If I recall correctly, I complained about this on the FOM several times before McLarty took up the challenge. Once he announced that Wiles’s proof could have the Universes axiom eliminated, there was even less pressure on the number theorists to provide the details of this, but it is still improper of them not to have noted the issue when writing about Wiles’s result.

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. 

It would be helpful if a number theorist fully conversant with all the top-level work in this area would state for the record if there was any theorem about objects of finite type that anyone had published with a proof using the Grothendieck technology for which the question of whether it was a theorem of ZFC was considered open.

— JS

Sent from my iPhone

> On Jan 6, 2018, at 11:34 AM, Arnon Avron <aa at tau.ac.il> wrote:
> 
> 
> Many thanks to Colin and Tim for their prompt and useful replies. Colin
> has also promised me (in a private letter) that he will add a link in
> his webpage to this paper, and said that it should indeed be
> submitted. I do
> hope that he will do so, because I, for one, find the current
> situation unbearable.
> 
> Some comments concerning Tim's reply:
> 
>> Arnon Avron wrote:
>>> It is generally agreed that Fermat's last theorem was proved more
>>> than 20 years ago. However, the original proof uses concepts and
>>> Means that go well beyond ZFC.
>> 
>> If you want to distinguish carefully between 'knowledge' and
>> 'belief' then I would maintain that your second sentence above
>> expresses only 'belief' and not 'knowledge'.  Brian Conrad, who has
>> a deep understanding of the proof of FLT, will swear high and low
>> that nothing beyond ZFC is used. The only concept that might figure
>> in the proof of FLT that goes beyond ZFC is an uncountable
>> Grothendieck universe, and Conrad will tell you that the existence
>> of such a thing is not used in the proof of FLT.
> 
> This is not what I understood from the 2010 paper of Colin,
> or from what I have read about this issue here on FOM and elsewhere.
> What is more, had it been clearly the case that officially
> and unquestionably   the original proof
> did not use anything beyond ZF (in particular: Grothendieck's
> axiom of universes), then Colin might not even had started
> his research on the subject. In any case,
> you do not even say that *you* know that nothing beyond ZF is used,
> but only that you rely on the swear of someone who, as you testify,
> has deep  understanding of the proof. With all respect, this
> is not mathematical evidence. Just relying on the swear of somebody,
> be it even Goedel himself, is  against the spirit and moral
> of mathematics. May   Brian Conrad (or anybody else that can) write please
> a detailed exposition of the alleged proof of FLT from ZF
> that substantiate   these claims? It will be nice if
> at the same time he makes the alleged
> proof more accessible to the overwhelming majority of the
> mathematicians in the world, so that everyone with Ph.D in mathematics
> who is ready to devote a reasonable amount of time (6 months or so,  say)
> to this goal, will be able to check the proof for correctness and for
> realizing
> what exactly is assumed in the proof. This is what happened in the past
> with every important mathematical theorem, and I find it very
> strange and very worrying that more than 20 years after the
> publication of Wiles's work, nothing like this has happened
> (as far as I know),  and the only significant progress that
> has been made is hidden in an unpublished
> work, the existence of which I could discover only after
> sending explicit questions to FOM.
> 
> 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.
> 
>> Angus Macintyre has, I believe, given talks about this subject---
>> 
>> https://www.cs.ox.ac.uk/seminars/355.html
>> http://www1.maths.leeds.ac.uk/pure/logic/abstracts/angus.html
>> 
>> ---but I have not seen anything in writing, or even a publicly
>> available video recording of a talk.
>> 
> 
> Again, I do wonder why.
> 
> Arnon
> 
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom