[FOM] Is Wolfram and Cook's (2, 5) Turing machine really universal?
Timothy Y. Chow
tchow at alum.mit.edu
Tue Oct 2 22:30:13 EDT 2012
Dominic Hughes wrote:
> I'd point to the proof of Fermat's Last Theorem as exemplary. By
> writing everything down in detail by 1993, a critical bug was caught,
> and repaired by the time of the final Annals of Mathematics
> publication(s) in 1995.
I don't think that Fermat's Last Theorem is quite the exemplar you
envisage it to be. By the "young undergraduate" standards you're talking
about, there are enormous leaps and gaps in the proof. The bug was not
found by "writing everything down in detail"; if it had, Wiles would
surely have caught the mistake himself. What actually happened was that
he wrote down enough details to convince himself and to meet community
standards for this kind of thing. Then referees studied the proof and
caught the error in the process of trying to understand it.
Short of a machine-verifiable formal proof, what constitutes a "fully
detailed proof" is in the eye of the beholder.
More information about the FOM