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."
I think that in far future all science will be done by AI, because knowledge will be too complicated and complex to understand for even most inteligent human on chemical boost/genetic engineered/stuffed with chips.
What modern Obelix would say today? Of course, "Those crazy Americans!".
...From TFA if a computer is used to make this reduction, then the number of small, obvious steps can be in the hundreds of thousands--impractical even for the most diligent mathematician to check by hand. Critics of computer-aided proof claim that this impracticability means that such proofs are inherently flawed.
So basically what they are saying is that if the proof is too long to be checked, then it is flawed? WTF?
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."
Short, sweet, beautiful proofs of interesting and useful theorems, I would welcome them to do so with open arms.
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.
John_Chalisque
To do that.... well, just make sure the program was designed by a correct computer.
Since you're going to need a human to write the proof of correctness for the program that wrote the other proofs, aren't you now?
Anyway, the entire point of a proof is to be read by humans. This isn't like, say, a computer program, where the point of the proof. A mathematical proof is something humans create in order to convince other humans of things beyond all doubt. The four color theorem proof was pretty closely watched; I guarantee you if you just go up to someone and say "statement [i]blah[/i] because my expert system verifies it to be the case" there is going to be some fucking doubt still there.
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!).
During my preparation for my interview to study Mathematics at Cambridge last year, one of the discussion topics that came up was computer-aided proof. Between the interview-experienced teacher, a school colleague who was also applying and myself, we came to the idea that computer-aided proof might not be proof at all, because proof for Mathematicans is the ability to reproduce the workings by yourself - it might take a very long time, but the idea should be that a human could dervive them in order for them to be considered true proofs of human concepts. Whether many in the Mathematical community in England take this view, I won't know until the end of the year when I hope to start my course - but based on this debate, it wouldn't surprise me if quite a few did.
Mattb90
Editor, allaboutgames.co.uk
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.
No, they didn't "prove" any such thing - you've been reading too much Roger Penrose if you think so. There's absolutely no evidence that human minds have magical access to truths which formal systems don't; there once was a time when it was thought "obvious" that parallel lines could never meet, and it's still hard for many people to believe that there is no such thing as universal time.
Who the hell came with this stupid name for the post?
The article is about computer-aided proof, where the human makes the essential proof decisions while letting to the computer the tasks of properly formulating and performing very simple, yet laborious steps (which would otherwise draw the attention of the human from essential stuff).
You **cannot** actually prove a really complex theorem in a fully automated way, because the reasoning is non-monotonic, which implies huge computational complexities. Machines are not yet good at being creative.
Because if there's one thing that humans are better at than computers, it's performing large numbers of repeated steps. Flawlessly.
Intelligent Design: because MATH is HARD.
To the opponents of computer-aided proof (with their hard-to-check argument), I would say this:
It's easy to check a proof. It's hard to come up with a proof. Computers are great at checking proofs - all the program needs to do is verify whether the steps are logically correct or there's a discrepancy. Coming up with a proof, on the other hand, is a very hard task (being NP-complete, unless defined in a certain way) and thus usually requires a human (or sometimes, a lot of humans) to work on the problem.
A computer would not be able to come up with new principles of mathematics in order to tackle a given problem, it would only try to use every trick that has been discovered to the point of creation of the program (of course that doesn't have to be the case, but my point is that human intervention would be required to "teach" the computer about the new concept so that it would try to use it for the proof)
That is not to say that computers are useless in proofs. Obviously, they're often used as assistants in proving something-or-other, but there's also a direction in computer science where your computer would take a program that you wrote in a certain manner, and prove certain properties about it, e.g. that it is not possible to get out of array bounds in your C program...
*yawn*
time to sleep
Did you know that "FTW" ("for the win") is a direct translation of "Sieg Heil"?
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.
If by left-wing you mean "gun-toting, Europe-hating, and neoliberal", then I agree with you.
I was surprised to find on ./ a title such as "The End of Mathematical Proofs by Humans?", but after reading the article i realized that the computer is only beeing used to speed-up calculations and the ideas are still born in the analogic human brain.
I have always used computer programs in math to solve equation, to probe combinatorial game theory problems, etc... When you find a way to make the computer "invent" proofs, just let me know, i'll call it AI.
Wondering why i am doing so strange posts? I am trying to get a "+5,Flamebait" or "-1,Insightful" rating.
This is dumb. Godel showed that there are non-standard models of arithmetic. This means that there are distinct, non-isomorphic sets of objects which satisfy the axioms of Peano arithmetic. There's no talk of formal systems in his proof.
Turing applied Godel's work to Turing machines and showed that there are non-recursive functions. No talk of formal systems here.
I have no idea why you're mentioning Cohen, since his most famous work had to do with showing that there are models in which the Continuum hypothesis fails and models in which the Axiom of Choice fails. Not related to formal systems at all. Just Zermelo-Fraenkel set theory.
All of this is tangential. Assuming a generous reading of "formal system" as "formal logic, your alleged "limitations" to formal systems come down to a simple corollary of Godel's completeness theorem: Given a fixed set of sentences S, there is a proof of A from S iff A is true in every model of S.
After all, I am strangely colored.
Perhaps the most difficult part in my own work as a mathematician is understanding an area well enough to create meaningful, interesting conjectures. In many cases, the proof falls out immediately. This obviously isn't universally true (e.g. Fermat's Last Theorem), but the mathematicians that I have the most respect for are the ones who are able to see the connections between seemingly unrelated areas and ask the right questions to pull it all together.
As other have said, computing may be able to verify an existing proof, but I think the real creativity and beauty in mathematics is often found in the initial formation of the conjecture.
First off, Moore's law may not hold out for another 30 years, let alone 60.
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.
http://rareformnewmedia.com/
don't produce proofs. They produce insights that make proofs feasible.
An insight that enabled a five page proof of Fermat's Last Theorem using nothing more than high school algebra would be a major result, even though much more complex proofs exist.
Post may contain irony: discontinue use if experiencing mood swings, nausea or elevated blood pressure.
As a maths degree student I can confirm that a very large portion of mathematics is devoted to finding new metaphors and angles of attack for a given situation.
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.
For the love of God, please learn to spell "ridiculous"!!!
Anybody involved in computers needs to learn this one important fact: AI fanatics time and again over promise and over sell their trade. Every few years, you get another AI snake oil salesman trying to claim that the turning point is just around the corner. But people that are actually educated in the problems at hand, those who have actually seen what AI has promised and can do, realize that it is all hype!
Proof generation can only be partially automated. It still requires massive human intervention, from choosing what to prove and then how to go about proving it. When you have computers automatically generating a proof of, say, Godel's Incompleteness theorem, it is actually a computer that was fed an intricately encoded version of of the theorem, along with some form of hint as to how to go about proving the theorem.
Not to mention that there is little use in a computer re-proving something that has already definitively been proven.
The difficulty arrises from the fact that there are absolute limitations to what computers can do. These limitations have been proven many decades ago... BEFORE THE CREATION OF ELECTRONIC COMPUTERS! But to the ignorant, these theoretical limitations do not matter... simply because they do not understand how absolute they are.
So again, learn this, you will time and again hear AI snake oil salesman spouting off crap about automating mathematical research and automating programming, etc. (Both are in a sense equally difficult as proofs can be seen as programs and visa versa.) In reality, at best, automated theorem proving is actually a tool that can be used to help mathematicians and computer scientists to do what they have been doing already. The level of automation varies, but in general is very low.
A human still has to drive the entire process, similar to how a car automates walking, but doesn't automate where to go and how to get there.
A computer can prove any theorem, if you give it long enough.
Reason: a theorem is a statement which has a proof. A proof is a finite sequence of logical statements. You can order all sequences of logical statements by lexicographic order within the sum of the number of variables used and the number of statements; then simply have a computer run through all sequences of logical statements in that order, checking each one to see whether the statements in the sequence are either axioms or follow by the rules of logic from the axioms, and checking whether the final statement is the statement you want to have proved. The computer will eventually reach a proof of whatever theorem you asked it to prove. Note that if you asked it to prove a statement which is not a theorem, it will never stop. Goedel's theorem tells us that there are some statements where not only will the computer fail to prove the statement true, it will also never prove the statement false.
The problem with trying to do this in practice is that for any interesting problem the shortest proof might not fit in a telephone directory - and the computer would be trying to find it by checking through all sequences of that size. It would take far too long.
The theoretical problem you refer to is whether one can write a program which will correctly classify all statements as true or false - this is not possible; some statements are neither. If you allow it to classify as 'neither' as well, it is still not possible - the sketch above will never classify any statement as 'neither' because with such statements it never halts, for example. Turing proved that no program can correctly classify all statements.
As an example of this technique was investigating the local clasification of maps from the plane to the plane, which I took part in at Liverpool Uni. Here we were looking for special cases in a four parameter family of maps. I.e. there were four numbers you could change and each set of parameters gave a different mapping. Using visulisation programs on a computer I managed to find a special case which had not been found before. When I showed the pictures to the rest of the dept no one beleived them as they seemed to contradict the theory. Was is a bug in the software, a misleading piciture or a bug in the theory?
In the end the experimental pictures proved to be correct and the theory was improved to account for it, involving lots of pen an paper mathematical work.
This sort of investigation is a long way from the grand formal proofs in the article. But perhaps more indicative of the way that computers can be used to inform mathematics. More like the experimental physics/theoretical physics devide. In this case is generation of a counter example.
One of the big problems with using computers is infinity. Most interesting problems in mathematics involve an infinite number of cases. Fermat: a^n+b^n=c^n four countably infinite numbers (integers). In the map case above it was four real numbers (uncountable infinities) Furthermore theory had proved that the underlying problem (all posible maps), which involved a countably infinite number of parameters which could all take an uncountable infinite number of values, could be reduced to just four parameters. Even with Moore's law its going to be hard to check all those cases. In the four colour theorem there is an infinite number of pattern to considered, the real smart bit in the theorem was showing that these could be reduced to just a finite number of special cases. In the clasification of simple groups we have several infinite of groups and a few (26) special cases.
Infinity will also show its head in formal methods. More to the point combinitoric complexity. As the number of symbols in the formal sequence increases so the numeber of cases you need to consider grows rapidily, hints of NP-hard problems here and testing for primeness. This makes thing hard when you start with a few axioms and try to find all the logical consequences.
Personally I don't have a problem with either of the proofs mentioned in the article. Both follow the same pattern, 1) reduce an infinite number of cases to a finite number of cases, 2) then check those using a computer. I can check the mathematics of 1) and write my own program to check 2). Hopefully the code's open sourced as well. Doesn't mean their particularly satisfying proof, or particually elegant, 10,000 special cases does not really flip my mathematical switch. Classification of simple groups does have a more elagant result, and deeper consequeces. Wilke's proof for Fermat, and the more interesting underlying conjecture, though long, is much more elagant, and more to the point much deeper opening up a whole new field.
End of the day, its another one of the typical stuff we get in the press. Nothing much new here. This debate on four colour theorem's computer proof has been around for a good while now, and mathematics has for the most part gone on as normal.
There are four sorts of people in the world: fools, lunatics, idiots and morons. - Umberto Eco, Foucaut's pendulum.
Proofs give correctness. Good proofs give insight.
Insight is what drives math forward; a clever and insightful proof is vastly better than a merely correct one.