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

[Timothy Y. Chow]

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.

> 1) Has McLarty's work and proof been published? If so - where?
>   (All I could have found on the intenet is his 2010 paper,
>   in which his result stated above is not mentioned.)

McLarty's paper is on the ArXiv but I don't know if it has been formally 
published: https://arxiv.org/pdf/1102.1773.pdf

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.

Tim