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

[James Smith]

Hi,

On 12/01/18 13:20, Tennant, Neil wrote:
> The blow-up factor from informal to formal proof looks to be two or three orders of magnitude, even for such a
> simple and informally compelling result as the irrationality of sqrt(2). One shudders to think what the blow-up factor
> (for faithful formalization) would be for the current informal proof of FLT!
>
> So much for "structurally homologous" formalizations of informal proofs.
This is a misunderstanding and often the complete opposite is true. 
Formalised proofs can be "orders and magnitude" simpler and more 
structured. See here...

https://mathoverflow.net/a/281884/93609

...and the link again:

[Prof. Thomas Hales - Lessons learned from the Formal Proof of the 
Kepler Conjecture](https://www.youtube.com/watch?v=Is_lycvOkTA)

I feel that it's important that more mathematicians accept this state of 
affairs rather than deny it.

Personally I feel that when proof assistants become more useable, making 
the work of Hales and others more accessible to mainstream 
mathematicians, debates such as this one will be a thing of the past. I 
long for that day...

Regards,

James