[FOM] Mathematical Experiments.

[Dan Goodman]

Bill Taylor wrote:
>... Even cases where computer proofs have (so far) turned out to be
> indispensable, such as the proof of the four-color theorem, are of this
type.
> They could easily be humanly checked, but no-one wants to waste the
effort.

The thing is that the 4CT proof couldn't "easily be humanly checked". A
human checking the computer proof of the 4CT would be more likely to make a
mistake checking it than the computer. One can imagine a human checking it,
but it's not actually possible. Is this significant? I think so, but I
expect most people on this list would disagree. At the very least, it shows
that when you say the 4CT "could easily be humanly checked" you probably
have something else in mind, e.g. there is nothing "in principle" stopping a
human from checking it, no individual step in the calculation is
unsurveyable by a person, only the calculation as a whole.

I'm not disagreeing with your central thesis, that maths and science are
different, but I think I disagree with your reasons. I don't think Lakatos
was trying to say that maths and science were the same, he was just pointing
out that the process of mathematical discovery is similar to that of
scientific discovery. What makes it different is that what changes in the
process of mathematical discovery is not the truth or otherwise of theorems,
but the choice of theorem to look at. In "proofs and refutations" he traces
the changing statement of Euler's theorem, not the change in the seeming
truth value of some particular statement of it. Examples, essentially
pictures, are the driving force for the changes, in his account.

Dan Goodman