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

[Arnon Avron]

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