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

[Freek Wiedijk]

Dear Revantha,

>Is it the concern that if the well-known results are introduced as
>"axioms", then some incorrect entry might introduce a false claim?

Yes, it is my experience that it is very hard to get
statements like this fully correct if you do not actually
formalize the full proof of everything.

Formalisations are very much like computer programs, but the
"outcome" is basically one bit ("yes, this is correct"),
unlike computer programs where the outcome is something
you can run.  So if you do what you propose (and everyone
else always proposes this too), then you taint that bit,
and are left with basically not much.

OTOH, Tom Hales "formal abstracts" project is quite close
to what you propose here.

Freek