Slashdot Mirror
The End of Mathematical Proofs by Humans?
vivin writes "I recall how I did a bunch of Mathematical Proofs when I was in high school. In fact, proofs were an important part of Math according to the CBSE curriculum in Indian Schools. We were taught how to analyze complex problems and then break them down into simple (atomic) steps. It is similar to the derivation of a Physics formula. Proofs form a significant part of what Mathematicians do. However, according to this article from the Economist, it seems that the use of computers to generate proofs is causing mathematicians to 're-examine the foundations of their discipline.' However, critics of computer-aided proofs say that the proofs are hard to verify due to the large number of steps and hence, may be inherently flawed. Defenders of the same point out that there are non computer-aided proofs that are also rather large and unverifiable, like the Classification of Simple Finite Groups. Computer-aided proofs have been instrumental in solving some vexing problems like the Four Color Theorem."
Much of mathematics isn't just grunt power, there is also a lot of creative work going on there. Without humans to drive the computers doing the work in the right directions, it could take a long time before a computer would be able to get its proof - it simply doesn't know what it is looking for.
I for one welcome our new robotic theorum proving overlords.
Quoth the server, "404."
Yes, thats right.
If you can't independently examine and verify your "proof" then how can it be considered proof of anything?
[)amien
I remember how much I hated learning alegebra, trig, calculus etc & how much the theory sucked, I never saw any point to it & loved it when I discovered my TI-83 could do pretty much everything.
Although I discovered easier ways to do the arithmatic, I still knew the underlying theory of the equations & what the numbers were actually doing, not just what a computer was telling me.
Students should learn this, they are the basic building blocks of a science that dictates pretty much everything on this planet & although they won't have a use for everything they are taught they will have enough knowledge to "problem solve" which is what most of high school maths is designed to do, it trains our brains to think logically & be able to work out complex problems.
How are people going to be able to further phsyics, medicine, biology if they get into their respective tertiary courses without understanding the basic principals of all science & have to learn it all over again??
Or what about when computers just won't work & things have to be done by hand??
Its fair to integrate comuters into maths but not at the expense of the theory that makes us understand how things work, we should not put all our faith in technology just because its the easy thing to do.
I concur. Math will always be about insight. The best math is simple and shows why the result is true. Most mathemeticians are unsatisfied by the four-colour proof because it does not satisfy these two conditions. Even if computers are eventually able to discover such proofs, mathematicians will still have to ask the computers to search for them. We must remember that problems like solving certain differential equations used to be difficult and involved, but now thanks to computers, we don't have to worry about them as much. The same will apply for very specialized results. The big theorems will still be up to humans to prove. Think of computer- assisted math as a kind of spellchecker or Googe suggest. Computers replacing mathematicians completely is about as far-off as computers replacing poets or historians.
The toad can't burp - and for some reason can't fart either, so it swells up and eventually explodes. --Anonymous Coward
In general, it is impossible to prove that such a 'formal logic validator' is correct since it is not possible to prove that an axiom system is correct inside that axiom system (one of Goedel's theorems). So if you would find a proof that your validator is correct, you'd have used reasoning techniques outside the logic of your validator, and do you believe those? (If so, why didn't you include them in the validator, since now your validator clearly does not support a reasoning technique you considered valid in the first place!)
Basically, at a certain point, you just have to "believe" that your axioms, logic, whatever you call it, is consistent. Because to prove it, you'd again need axioms, a logic, etcetera, ad infinitum.