| dbp:text
|
- …if we accept the [Four-Color Theorem] as a theorem, we are committed to changing the sense of "theorem", or, more to the point, to changing the sense of the underlying concept of "proof". (en)
- …[the] use of computers in mathematics, as in the [Four-Color Theorem], introduces empirical experiments into mathematics. Whether or not we choose to regard the [Four-Color Theorem] as proved, we must admit that the current proof is no traditional proof, no a priori deduction of a statement from premises. It is a traditional proof with a lacuna, or gap, which is filled by the results of a well-thought-out experiment. (en)
- Suppose some supercomputer were set to work on the consistency of Peano arithmetic and it reported a proof of inconsistency, a proof which was so long and complex that no mathematician could understand it beyond the most general terms. Could we have sufficient faith in computers to accept this result, or would we say that the empirical evidence for their reliability is not enough? (en)
|
