[FOM] Nelson's proof assistant

David Roberts david.roberts at adelaide.edu.au
Sun Oct 19 20:28:11 EDT 2014

I'm not sure if people know, but Nelson passed away last month.


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.



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

More information about the FOM mailing list