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."
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.
This reminds me of a Nature paper from last year:
Functional genomic hypothesis generation and experimentation by a robot scientist
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."
You linked to a "by invitation" editorial. That doesn't necessarily represent the normal views of the magazine. Have you got any further evidence they generally support Lomborg's views?
What do they use for this field? Prolog still or something new(er) has been invented? Or they do what businesses do and use whatever comes handy or whatever is the current fad?
I agree with (1), I believe Godel had a hand in that one.
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.
Reliable, Great Value Hosting: $7.95/mo 2.4G/120G
What you and others fail to grasp is that computers are evolving rapidly, human brains aren't. Our current computers are still far from having the data processing capability of a human brain.
In rough orders of magnitude, a human brain has 1e11 neurons, with 1e3 synapses each, doing 1e2 operations per second. Considering that a neuron can be emulated by a multiply-add operation, we would need 1e16 such operations per second to emulate a human brain.
A 3 GHz Pentium can do 1e10 floating point multiply-add operations per second, so a human brain is roughly equivalent to one million desktop computers. Therefore, Moore's law tells us that we still need 30 years of progress before we have a human-equivalent computer, but in 60 years a desktop computer will have the data processing power of a million human brains.
We have absolutely no way to predict the consequences of this. But I'm sure that, unless we connect our brains directly to computers, we will be left hopelessly behind.
> By programming my computer to independently examine and verify the proof. Done
> 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
and the bug was reported on October 30, 1994
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.
I recall a story I once read by Issac Azimov about a future culture where all knowledge of mathematics has been lost to humans, who have to rely on computers and calulators to do even the simplest math problems (older computers make the new computers and humans are left completly out of the process).
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?
Technoli
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.
You need to restart your computer. Hold down the Power button for several seconds or press the Restart button.
It is very easy to produce a validator which correctly classifies valid and invalid proofs written in formal logic. It is very easy to prove that the validator does what it is meant to do.
We don't know whether this abstract formal logic thing actually has any resemblance to the real world - that is not Goedel's theorem, which assumes logic to be valid and discusses potentially interesting frameworks for mathematics. Whether formal logic 'works' is simply something you have to believe, you cannot argue it, for the obvious reason. Whether you can use formal logic to demonstrate that your mathematical axioms are consistent is not obvious; Goedel's theorem states that in fact whenever your mathematical axioms are strong enough to produce interesting mathematics, you cannot demonstrate consistency.
The reason why mathematicians do not like computer proofs (as much as normal proofs, anyway) and do not like computer validation (always) are:
Computer proofs tend not to give any insight into why a statement is true. They simply check vast numbers of cases, when there might exist a simple argument which gives understanding. However, there is usually interesting mathematics involved in reducing the original problem to something which can be computer checked.
It is not easy to produce a program which will verify a proof written by a normal person, in the same way that it is hard to write a program which can spot contradictions in any argument written in natural English.
An argument written out in formal logic, although easy to verify for a computer, is generally much, much longer than the same argument written by a normal person, and even if you wanted to read the telephone-directory sized proof, the interesting ideas are so dispersed that you would gain no understanding from the proof.
So, a computer verifier would only be useful when a proof is written in formal logic - which only a computer would do for a proof of any interesting statement. But the computer proof won't give a mathematician any understanding of why the statement is true, so the mathematician doesn't like it. Furthermore, because formal logic is so long-winded, it doesn't seem likely that a computer will ever be able to prove interesting statements by doing a simple bash out formal logic until it works approach. IMO, a computer program which can prove interesting mathematical statements in sensible amounts of time will be about as hard to write (and probably not too dissimilar to) a Turing-capable program.