[FOM] Is Wolfram and Cook's (2, 5) Turing machine really universal?

[Vaughan Pratt]

On 10/2/2012 7:30 PM, Timothy Y. Chow wrote:
>
> Short of a machine-verifiable formal proof, what constitutes a "fully
> detailed proof" is in the eye of the beholder.

As machines increase in intelligence, what constitutes a 
"machine-verifiable formal proof" is surely in the eye of the machine.

Hughes asked for a "rigorous proof of weak universality."  He defined 
this as "something a young undergraduate could work through centuries 
from now, long after we're all dead and gone, and be 100% convinced of 
the result."  And he pointed out that "Neary and Woods are refreshingly 
honest about the lack of a rigorous proof in their 2009 paper."

There's a big difference between a proof that is not rigorous because it 
does not conform to some system of axioms and one that contains lacunae 
that can't be filled straightforwardly.  The shortcomings of the extant 
proofs would appear to be in the latter category and not at all in the 
former, which no one is asking for.

Vaughan Pratt