Are Computers Ready to Create Mathematical Proofs?

DoraLives writes "Interesting article in the New York Times regarding the quandary mathematicians are now finding themselves in. In a lovely irony reminiscent of the torture, in days of yore, that students were put through when it came to using, or not using, newfangled calculators in class, the Big Guys are now wrestling with a very similar issue regarding computers: 'Can we trust the darned things?' 'Can we know what we know?' Fascinating stuff."

Comments

Mathematics is Human

[Traser]

Mathematics is one of the most intensely human of human endeavours. Everything in it is a production of the human mind entirely. Yes, the real world can sometime lead us into an interesting area of inquiry, but at its core the uncoverings of truth from axioms is a human endeavour.

A computer can be a useful tool (I'll be doing computational graph theory this summer), but it is not human. It does not have the ability to hold the possiblities of ideal forms within it and understand. It does not think.

The use of numeric methods to solve applied problems, or symbolic methods to pure problems is good and useful, but it does not constitute proof.

A human being, given an understanding of the underlying mathematics, must be able to go through the proof step by step, and see that, from the givens, the conclusion is inevitable.

I don't accept the Four-Colour theorem as proven true. I strongly suspect it to be so, but my suspicion does not truth make.

The Riemann hypothesis, on the other hand, is much, much further from being proved then the Four-Colour Theorem. Yes, millions of zeroes have been checked...but there are infinitely many zeroes, and all it takes for it to be false is for ONE of those zeroes to fall off the Re=1/2 part of the complex plane.

If I were giving odds, then millions divided by infinity is awfully close to zero.