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

[Robert Solovay]

Freek,

Can you give a link to Hales' "formal abstracts" program?

-- Bob Solovay

On Jan 19, 2018 4:24 PM, "Freek Wiedijk" <freek at cs.ru.nl> wrote:

> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180120/8e44c7e2/attachment.html>