Slashdot Log In
The End of Mathematical Proofs by Humans?
Posted by
timothy
on Wed Apr 06, 2005 03:27 AM
from the somehow-I-doubt-it dept.
from the somehow-I-doubt-it dept.
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."
This discussion has been archived.
No new comments can be posted.
The Fine Print: The following comments are owned by whoever posted them. We are not responsible for them in any way.
Full
Abbreviated
Hidden
Loading... please wait.
Critics Reaction... (Score:5, Insightful)
So basically what they are saying is that if the proof is too long to be checked, then it is flawed? WTF?
Re:Critics Reaction... (Score:5, Insightful)
If you can't independently examine and verify your "proof" then how can it be considered proof of anything?
Parent
Re:Critics Reaction... (Score:5, Informative)
If you can't independently examine and verify your "proof" then how can it be considered proof of anything?
That's easy. Speaking as a PhD mathematician, there's nothing disturbing at all about these computer proofs. They're examples in which a computer was programmed to generate a perfectly standard proof, except that it's extremely long.
Checking the proof is not hard: it suffices to verify that the program emits only correct inferences. That's nothing more than a standard human-generated proof. In addition, a verifier can be coded by someone other than the original author, to check the validity of the inferences generated by the first program. The checker's algorithm can also be verified using a standard human proof, and would be used to confirm that a bug didn't result in an incorrect proof.
Note that Gödel's incompleteness theorem has nothing to do with these programs: they don't generate all possible proofs. They only generate one specific type of proof per program. Each program is easy to verify.
You could call the software correctness proofs "meta-proofs", but that's just being coy. They're perfectly legitimate proofs, and they are sufficient to prove the correctness of proofs generated by the program.
Parent
Re:Critics Reaction... (Score:5, Interesting)
> properly, the instructions for a computer to verify a proof can be a lot simpler
> than verifying the proof itself.
But even multiple computers performing a verify isn't _truly_ a verification.
After all, how long did the Pentium division bug go _unnoticed_???
Looks like the chip was released on March 22, 1993 [wikipedia.org]
and the bug was reported on October 30, 1994 [wikipedia.org]
Over a year and a half worth of time any/all such verifications obtained with the newest intel computers at the time were WRONG.
And any guesses how they even found this bug??
It was a human, not another buggy computer, that had to verify the data.
Yes computers can do things faster, but ever underestimate the power of truly knowing what your doing, which so far, a computer can't grasp at all, let alone do as well as the human mind.
Parent
Re:Critics Reaction... (Score:4, Insightful)
Parent
"peer" review (Score:5, Funny)
Why not have it verrified by other computers?
Parent
Re:Critics Reaction... (Score:4, Insightful)
I could assert that 2+2=4. You may believe me, but have I really proven it to you? Not yet, so you don't need to believe me. If I instead say that the the cardinality of the union of two disjoint sets, each of cardinality 2, is 4, then I've (sort of) showed you that 2+2=4, assuming you accept my definitions of disjoint sets, set union, and set cardinality (which presumably I've proven elsewhere, or taken from some other source). Now do you believe me that 2+2=4?
I could assert anything. You may or may not know if it's true. A proof is just something to back up my assertion and convince you that I'm right. Hence, if a proof is unintelligable, it's pretty darn worthless.
Parent
Re:Critics Reaction... (Score:5, Informative)
- An abc (not THE abc, just one)
- formulas
- derivation rules
An axiom is just a derivation rule which derives from the empty set.Basically, a proof is, according to the axiomatic method, is just a non-infinite sequence of formulas, which can be created by the allowed derivation rules. The whole point is that a proof for A HUMAN, and mathematical proof is different. The axiomatic system is not perfect, either. The whole Hilbert [wikipedia.org]-plan is proven to be impossible to be done, thus it is not possible to prove that there are no contradictions in the axiomatic system
I think the "MUI" axiom system is commonly used to demonstrate how it works, basically. It is too lengthy, and i'm lazy.
Parent
Re:Critics Reaction... (Score:5, Informative)
Fully formal mathematical proofs depend on nothing but ability to distinguish characters, to compare text strings, and to perform substring substitution.
To your example (2 + 2 = 4). In formal arithmetics, based on Peano axioms, there is one primary operator, let's call it s:N -> N, and s(n) is interpreted as (n + 1). "2" is _defined_ as s(1). 3 is defined as s(2), and 4 is defined as s(3). So one has to prove that s(1) + s(1) = s(s(s(1))).
By definition of addition (remember, addition is not fundamental notion in the formal arithmetics, it's defined in terms of s-operator), a + s(b) = s(a + b), and a + 1 = s(a), so we have
s(s(1) + 1) = s(s(s(1))),
s(s(s(1))) = s(s(s(1)))
Q.E.D.
So, where proof above depends on anything but mechanically verifiable string manipulations?
P.S., of course mathematical formulae are not strings, but rather trees, but this doesn't change a bit.
Parent
Re:Critics Reaction... (Score:4, Informative)
Parent
Re:Critics Reaction... (Score:5, Informative)
So the question is - how are we going to prove/disprove a computer program that proves a theorem? Program complexity has meant that all but the most trivial programs cannot be 'proven'.
The solution, it seems to me, is per the article: get the s/w to output a series of steps using formal logic. Any series of formal logic steps should be confirmable by a 'formal logic validator', and that is the only program we need to prove correct. That will be non-trivial, but will then open the floodgates to any hacked up piece of code to be used to generate provable logic.
Parent
Re:Critics Reaction... (Score:5, Insightful)
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.
Parent
Re:Critics Reaction... (Score:5, Insightful)
Parent
Re:Another Lomborg case? (Score:4, Interesting)
Parent
Creativity (Score:5, Insightful)
I for one welcome our new robotic theorum proving overlords.
Re:Creativity (Score:4, Funny)
Parent
Re:Creativity (Score:5, Insightful)
To some extent that's true, except in areas where human understanding has reduced mathematical proof to a mechanical process. For example, verifying algebraic identities, or even geometric proofs. A more advanced example is the Risch algorithm for elementary integration. It amounts to a proof that an integral either is or is not expressible in terms of elementary functions. Eventually we come to understand an area to such an extent that we can implement mechanical algorithms and move on. The proper role of the computer is to carry out these algorithms, so that we can use them to discover something else.
Parent
If computers could write proofs... (Score:5, Insightful)
As a tool to produce vast quantities of precise logical porridge quickly, computers have no equal in today's world, yet that is not what real mathematical proofs should be about.
Mathematical proofs should show short, clever ways of connecting otherwise disparate concepts that are only obvious in hindsight. This is where computers will always be weaker.
Re:If computers could write proofs... (Score:4, Funny)
Parent
Re:If computers could write proofs... (Score:4, Insightful)
Parent
Seems simpler to prove proffs-by-computer (Score:3, Insightful)
To do that.... well, just make sure the program was designed by a correct computer.
Re:Seems simpler to prove proffs-by-computer (Score:5, Informative)
- Logical problems with proofs for correctness. For example, it has been proven that no program can prove itself correct.
- Correctness proofs are hard to do and incredibly tedious. Have you ever tried it? And no, you can't have a program do them, because you'd have to prove this program correct, which sends you right back to square #1.
- You'd have to prove all sorts of other factors correct, including the operating system and hardware your program is running on. This leads to another set of interesting problems, including that "correct hardware" is useful only as a theoretical concept. What's a "correct computer" if there's a small probability that bits will spontaneously flip in memory, for example?
In short: while it might seem elegant to prove the prover, then have everything else proved by this prover, this approach has little value in practice.Parent
Re:Seems simpler to prove proffs-by-computer (Score:5, Interesting)
With (2), the program can reduce the tedium of proving the original proof in some cases. That's what computers are good at and are better at than humans. Proving the program may well be much easier. I would think that's why the researchers in the article used computers in the first place. If you program in C++ you will have a problem, but a functional or logic language program is straight-forward to prove (PROLOG programs are essentially the execution of a proof).
With (3) you could show by running it on different hardware and software that the platforms did not affect the result by a huge probability. If you don't like the 'probability' bit, who says there isn't a human trait or gene that causes any human to get a proof wrong? Humans are imperfect too, but if enough of them agree, and they are qualified, then we agree that what they agree on is true. This is the same situation as the potentially flawed platforms problem.
Parent
Here's a good theorem prover (Score:5, Informative)
The best math is always elegant. (Score:5, Interesting)
What about Fermats last theorem? Fermat wrote in the margin of his note book that he had a proof, but it was too large to fit there, so he'll write it on the next page. Trouble was, the next page was missing from the book.
The modern proof for FLT took hundreds of pages of dense math and went through some math concepts that AFAIK hadn't even been invented in Fermats time.
What was Fermats proof (if it existed)? It would surely have been far more elegant than the modern version.
That doesn't make the modern version wrong, just less pure, I feel.
The problem with modern computer aided proofs is they allow the proof to become unwieldy and overly verbose, compared to what it would have to be if just a human produced it.
Such is progress I guess.
Re:The best math is always elegant. (Score:3, Funny)
Re:The best math is always elegant. (Score:5, Insightful)
Parent
Re:The best math is always elegant. (Score:5, Informative)
Mathematicians think they know what Fermat thought was the "proof" that he could not fit in the margin, since Fermat used a similar strategy for another problem. Euler was the one who used Fermat's strategy on Fermat's last theorem explicitly, and showed that it did not give a full proof as Fermat had hoped. It might be that Fermat himself tried and then gave up, or that he was happy to have "solved it" and looked for other things to prove.
I think you (and most people) misunderstand the reason Fermat's last theorem has such a central place in math history. But first lets discuss the reason why the problem became so well known; it is because it is such an easy problem to state and to understand, still no one has been able to use "simple" math to prove it. Even Fermat himself thought the problem should be fairly straigth forward to solve, and it has made generations of people with curiosity for math look for proofs and even thinking they have found one. It is also a problem some of the greatest minds of math did not manage to solve. Fermat, Euler, Lagrange, Gauss, Abel, Riemann, etc have all had a try and did not solve it. Which math wanna-be wouldn't want to solve something this group of people did not manage?
Now, even though this has made Fermat's problem something that has created a lot of publicity, the number one reason Fermat's problem has been important, is because of all the beautiful maths that have been discovered by mathematicians trying to solve it. Fermat's theorem in itself is not interesting. It is not like the Riemann hypothesis, which if proven to be false, will make much of modern maths not true or at least force mathematicians to look for new proofs. This is because you can prove much interesting stuff if you assume the Riemann's hypothesis is true, problem is of course, this is not yet proven. If Fermat's theorem was been shown to be not true, that would have been suprising, but would not made large parts of maths collapse.
So, the modern proof of Fermat's theorem is the end of a long journey which has lead to some very deep mathematical knowledge, and in a way, Wiles' proof is much more interesting in its own right than that it also proofs that Fermat was right in his guess. A "simple" proof (watch out when mathematicians use the word simple or trivial) of Fermat's problem would give undeniable bragging rights, since you could say you solved a problem Gauss couldn't solve with the maths Gauss knew. But again, it probably would be more of a huge accomplishment for one person than a huge breakthrough in maths.
A last comment; the reason Wiles' proof is long is not because math is verbose, far from it . It is because Wiles is able to connect what would seem to be two unconnected branches of mathematics, showing that problems in one of the branches can be restated as problems in the other. This is not something you do in a few pages. And the importance of it becomse clear, if you consider that what can be an unsolveable problem in the one branch of maths might be reformulated as a solveable problem in the other. Math is always about trying to find ways to solve something as simply as possible. Not something computers is very good at, so no Abel prize to Big Blue for a while I think.
Parent
Computer _aided_ proofs (Score:5, Insightful)
Computer proofs, like the graph color proof, are not proofs that are completely generated by a computer. The computer is merely used to brute force a fairly large number of 'special' cases which together account for all cases. The construction of the proofing method is and will remain human work, lest we create AI that matches our own I.In short, they are computer aided proofs only.
Further and more importantly, at this point we do not have and are not likely to have a machine that can prove any provable theorem (and fyi, not all truths in mathematics are provable!).
Are computer-aided proofs really proof? (Score:3, Insightful)
No progress without understanding (Score:5, Insightful)
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.
Blowhard critics could use a logic course... (Score:4, Insightful)
Because if there's one thing that humans are better at than computers, it's performing large numbers of repeated steps. Flawlessly.
Re:Blowhard critics could use a logic course... (Score:5, Insightful)
Anyway, the problem isn't the ability for the computer to perform flawlessly, the problem is in our ability to accurately specify to the computer what we want it to do. It's the whole "fast working idiot" thing, mechanical perfection isn't much good if we wind up just directing the computer to perfectly, flawlessly do the wrong thing very quickly. We have enough trouble convincing ourselves real-world software is going to do what we wanted it to after it compiles; and in that case we at least have the advantage we can run it and test it to see if it does what we expect. With software-generated proofs, not so much, since the program IS the test.
I think computer aided logic can be useful if we just think of a proof-generating software program as a funny, mechanically verifiable sort of abstraction, but you find yourself making an argument that rests on assuming that a computer program you wrote does what you think it does then this is problematic.
Parent
A proof needs to be intuitive (Score:4, Informative)
I doubt the human proof system will go away completely - even if we can check nasty theorem proofs using computers, we still need humans to sit and explain what they mean.
BTW, as a geek I want to know (Score:4, Interesting)
Re:BTW, as a geek I want to know (Score:5, Informative)
Parent
Issac Azimov story (Score:5, Interesting)
A janitor at a science lab rediscovers the 'ancient knowledge' on his own. The military quickly gets ahold of it and immediatly puts it to use in weapons research, whereapon the janitor promptly takes his own life in shame.
Anyone think there might be a future where humans rely on computers so much that they don't bother learning math at all any more?
Re:Science by AI (Score:5, Interesting)
Functional genomic hypothesis generation and experimentation by a robot scientist [nature.com]
The question of whether it is possible to automate the scientific process is of both great theoretical interest and increasing practical importance because, in many scientific areas, data are being generated much faster than they can be effectively analysed. We describe a physically implemented robotic system that applies techniques from artificial intelligence to carry out cycles of scientific experimentation. The system automatically originates hypotheses to explain observations, devises experiments to test these hypotheses, physically runs the experiments using a laboratory robot, interprets the results to falsify hypotheses inconsistent with the data, and then repeats the cycle. Here we apply the system to the determination of gene function using deletion mutants of yeast (Saccharomyces cerevisiae) and auxotrophic growth experiments. We built and tested a detailed logical model (involving genes, proteins and metabolites) of the aromatic amino acid synthesis pathway. In biological experiments that automatically reconstruct parts of this model, we show that an intelligent experiment selection strategy is competitive with human performance and significantly outperforms, with a cost decrease of 3-fold and 100-fold (respectively), both cheapest and random-experiment selection.
New Scientist also had an article on it: "Robot scientist outperforms humans in lab." [newscientist.com]
Parent
Re:Science by AI (Score:5, Insightful)
Parent
Re:Science by AI (Score:5, Insightful)
Parent
Re:Science by AI (Score:5, Informative)
It has been PROVEN (and it's a well-known fact) that it's impossible to create a Turing machine which will determine if a given expression is true or false (see Incompleteness theorem [wikipedia.org] for details).
For example, it's impossible to find answer to CH [wikipedia.org] (continuum hypotesis) in ZFC (Zermelo-Fraenkel + Choice axiomatics).
In short: some problems can't be solved in existing theories, they require creating a new theories with new axioms. It's non-formalizable process (it's also proven), so no computer can do this.
Parent
Re:Science by AI (Score:5, Insightful)
This actually is more about the limitations of logic than the limitations of computers. Indeed, Godel's Incompleteness Theorem has nothing to do with computers--it is a proof that in any system of logic (that meets some very broad criteria) there must exist statements that are true but that cannot be derived from the postulates of the system by any sequence of logical steps. Adding additional axioms does not solve this; there always remain unprovable propositions. This limitation applies to proofs by humans as well as proofs computers. However, the fact that there are some theorems that cannot be proved does not mean that there are not many others that can be.
However, the fact that there are some truths that are literally inaccessible from the postulates certainly suggests that there may be others that are accessible only by a very large number of steps, effectively requiring computers. I wonder if anybody has ever attempted to prove this?
Parent
Re:Science by AI (Score:4, Informative)
The theorem says that there are either true unprovable things or things that are both provable and provable to be false. An interesting formal system is either incomplete or contradictory (it can be both, but it doesn't have to).
Parent
what about the software (Score:4, Insightful)
Secondly, how fast does software progress ? Suppose we all had computers 60 billion times faster than we do now. What would we do with them ? run SWING based java applications with tolerable responsiveness, play solitaire faster, run doom 5... [although the frame rate might be a bit low] ok... great,
Intelligence and computing power are orthogonal concepts: suppose you communicated with aliens who were a 100 light years away, would they be less intelligent because it too 200 years to get an answer. Anything you can do on todays supercomputers, you can do on pocket calculator [with enought memory].. it just takes longer.
Lastly, in the long run, computers wont outgrow our brains, they will be integrated with our brains.
Parent
Re:Science by AI (Score:4, Interesting)
Who's to say that neurons operate in the same way as a computer's multiple-add operations? Another little problem is that you'll need additional programming to tell the computer how to emulate the communication and interaction between neurons. I imagine that this would take far more processing power than we could ever achieve.
We may be able to emulate the parts, but you can't just throw the parts together in a heap and expect it to work. The sum of the parts is far more complicated than the parts themselves.
Parent
Metaphor (Score:5, Insightful)
This takes a ridiculous amount of pattern recognition skill (which is one area where computers tend to be outperformed by all comers) and the ability to find new ways to abstract data. A computer could possibly come up with an idea like more-than-3-dimensional space on its own, but I'd be very surprised if even the best one could think of something like topology or tensors on its own.
Production of unusual metaphors for things we thought we knew is a major driving force for the most important mathematical developments. It's not something I can see computers managing at any time in the near future.
Parent
Re:Science by AI (Score:5, Funny)
Yeah, right. The great AI machine will be delivered in the same week as my flying car. Taking orders now, please form an orderly queue.
According to rumors it will be bundled with Duke Nukem Forever.
Parent
Re:Godel/Turing/Cohen... (Score:3, Insightful)
Re:Consider the source (Score:5, Funny)
What does Slashdot know? It's a left-wing rag.
Parent
Re:Consider the source (Score:5, Insightful)
Secondly, the claim that a magazine that opposes the death penalty and supports gay marriage is right-wing rag (which presumably you meant in US terms, is kinda amusing.
The Economist, correctly stated, is a liberal magazine. It supports liberal economics and liberal social policy. Unfortunately the word 'liberal' in the US has been badly distorted.
Parent