[FOM] Nelson's proof assistant

[David Roberts]

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