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

[Josef Urban]

Hi Bob,

perhaps look at the links in the README at
https://github.com/formalabstracts/formalabstracts .

Tom has recently applied for a larger project funding for this. If you are
interested, I am sure he will send you the proposal.

Best,
Josef

On Sat, Jan 20, 2018 at 3:29 PM, Robert Solovay <solovay at gmail.com> wrote:

> 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
>>
>
> _______________________________________________
> 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/1a891ed9/attachment.html>