[FOM] Nelson's proof assistant

[katzmik at macs.biu.ac.il]

Unlike his proof, what is certainly not flawed is this excellent illustration
that computer code can only be as reliable as the programmer, which should
puncture any "absolute rigor" balloon in case any are still floating.  MK

On Mon, October 20, 2014 03:28, David Roberts wrote:
> I'm not sure if people know, but Nelson passed away last month.
>
> http://www.math.princeton.edu/news/home-page/professor-emeritus-edward-nelson-passed-away-september-10th
>
> I hope some of his unpublished work Timothy Chow mentions is preserved
> and made available, even if his claimed proof of inconsistency of PA
> is flawed.
>
> Regards,
>
> David
>
> On 16 October 2014 07:32, Timothy Y. Chow <tchow at alum.mit.edu> wrote:
>> A couple of people have asked for more details about Nelson's claimed
>> machine-verified proof of the inconsistency of PA.
>>
>> Nelson said that he used a proof assistant that he called "qea".  I think he
>> stated this fact in the (human-readable) outline of his proof that he posted
>> on his website; however, after he realized his mistake, he withdrew that
>> outline from his website, and I didn't save a personal copy, so I can't
>> verify directly what he said in there.  Fortunately, though, we have the FOM
>> archives:
>>
>>   http://www.cs.nyu.edu/pipermail/fom/2011-September/015818.html
>>
>> I don't know if Nelson ever released qea.  The link to the output of qea
>> still works as of today; I don't know how much longer that will remain true,
>> so someone may wish to archive it somewhere more permanent if it seems to be
>> of interest.
>>
>> Tim
>> _______________________________________________
>> FOM mailing list
>> FOM at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>
>
> --
> Dr David Roberts
> Research Associate
> School of Mathematical Sciences
> University of Adelaide
> SA 5005
> AUSTRALIA
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>