Re: Math as an Experimental Science


Chris Thompson wrote:
In article <1156928016.247397.38890@xxxxxxxxxxxxxxxxxxxxxxxxxxx>,
Proginoskes <CCHeckman@xxxxxxxxx> wrote:

Han de Bruijn wrote:
William Elliot wrote:

Riddle of the Day. If the statement of a computer discovered and proven
theorem, is so long and complex that nobody can read it, (ie, is
incomprehensible), is it meaningful and useful (does it really exist)?

Huh, huh. Riddle of the Day. How about Wiles' Court Room Style Proof of
Fermat's Last Theorem? And other such modern "proofs" ...

Including the Four Color Theorem proofs.

Feh. There's nothing in the least impossible about checking the RSST
proof (for choice) of the 4CT with pencil and paper. It would be
error-prone mostly because it would get so boring after the first
few hundred cases. Most of us prefer to check the programs used
instead ...

I know I did. (I'm in the acknowledgements of the main RSST paper.) For
my GRA, I went through the already-written program (in C) and rewrote
it in Pascal. I found a couple of bugs in the C code, but when they
were fixed, the proof still worked.

--- Christopher Heckman

Compare this with, say, the classification of finite simple groups,
widely claimed to involve so many thousands of pages of proofs
published in so many places that no one person has ever read and
checked them all. [This may, of course, be an urban legend. But it
certainly puts things like the 4CT in the shade.]

.