[FOM] Nelson's proof assistant

[Timothy Y. Chow]

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