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.
In the past, I've used the HOL Theorem Prover. It's a nice toy to play with if want to get started in this area.
Please login to access my lawn
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.
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!).
I have no doubt that in 50 years (given current progress), creativity as we know it will be commonly implemented in advanced computers. Your brain is nothing more than a biologically advanced computer, complete with binary nerve signals and the works.
Why can't human brain functions be copied and improved upon in circuitry, other than the currently prohibitive costs involved, and our failure to accurately determine the exact neuron mapping of anyone's brain. Even the dynamic neuron connections could be potentially emulated or mimiced by a computer.
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.
Theorem proving is NP Complete.
FOL Theorem provers jump through a number of hoops to make the whole bit a little more practical, but realistically speaking, having a computer that just runs through mathematical proofs in the manner that a human does is a long way off.
An interesting thing about the article is that the first proof was done with an FOL prover... it was a long, non-intuitive proof, but an FOL prover has performed that proof.
The second was done with code, a human had to write the program. There is no computer replacing the activity of a human in performing this action that I can see here. It was merely code to brute attack the problem from what I can see, but I didn't read the guys article (from what I can see, it hasn't reached publication yet anyway).
I'm certainly not a very gifted mathematician, but I'd like to think my grasp on it is at least adequate to make this point: from the proofs I've seen and understood, it seems that while the shorter and more elegant proofs may not strictly be more "truthful" than complicated ugly ones, the important thing is they are so much easier to understand, verify, and explain to others. For instance, I remember being especially charmed by Cantor's diagonal argument and will not forget that particular method of reasoning for the rest of my life.
But maybe there's a point where simple proofs just won't do it; if there were a 4 line proof for Fermat's last conjecture I'm sure someone would have found it before Andrew Wiles proved the thing in something like 80 pages.. In such cases, computer-aided reasoning is really the only way to go, I'd say. It's probably easier to verify a proofchecker than a proof.
Gosh, thanks. That must be why the other ships call me Meatfucker -- GCU Grey Area (Eccentric)
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.
:)
Nonsense. If people can't verify proofs, then what you need to do is to verify them by computer
I'm not entirely joking here - so long as the verification program is written independantly of the thoerem-proving program, and it can reliably distinguish between valid and invalid logical inferences, what's the problem? It's simple automated testing methods really.
My Karma: ran over your Dogma
StrawberryFrog
That's what they said 50 years ago too ...
Using computer programs to prove theorems in mathematics is as old as the field of artifical intelligence itself. In fact, some of the initial excitement around AI originated from the existence of such programs as Newell and Simon's Logical Theorist and it's sucessor the General Problem Solver .
IIRC - back in the early days of AI (1960s), some people in the field thought that in relatively short order computers would be a major soucre of such mathematical proofs. It hasn't happened yet, but that doesn't mean that it won't eventually.
I believe that Feigenbaum's constant was discovered with the aid of a programmable pocket calculator. He noticed something, and used the computer to check it out. I think that of all the things that computers can do for mathematicians, this is the most valuable. You can ask "what about this" and the computer will do the grunt work. It's made a grad student's life much easier I'm sure :)
In Soviet America the banks rob you!
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.
What does The Economist know? It's a right-wing rag.
What does Slashdot know? It's a left-wing rag.
"Nine times out of ten, starting a fire is not the best way to solve the problem." - my wife
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"?
A right wing rag that backed Clinton and Kerry (albeit grudgingly), supports gay marriage, legalisation of drugs, gun control, abolishment of the death penalty..?
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.
The Economist is the same magazine that supported Bjørn Lomborg, thereby proving their utter incompetence in environmental science. They defended him in spite of clear and very detailed indications from the scientific environment that he was nuts.
I suppose they will know economics when they talk about it, but they demonstrated an inappropriate habit of pontificating on things they don't have a clue about. I for one think they burned a lot of karma.
Victims of 9/11: <3000. Traffic in the US: >30,000/y
If you take a grad school AI course, they'll make you do proofs the way a computer does it... maybe using propositional logic. The idea is to break up the problem into a set of statements that looks quite ridiculous (e.g. NOT engine AND train AND NOT moving), and then taking pairs of these statements and mixing and matching. The result is that you determine your sequence steps by simple trial and error or by trying to combine the propositional symbols (AND, NOT etc) and the variables (train etc). Once you generate a proof, its just a list of such statements which evaluates to a FALSE or a TRUE value but if you want to understand the proof, its hopeless.
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.
I don't want to read
The most popular system for the computer-aided Formalized Mathematics is mizar. It even has it's own journal for proofs written with it.
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.
You mean... thinking?
Geometry wasn't the most useful of my high school math classes, but it was the most fun, because we all worked together to come up with proofs, showing that those lousy formulas we had to memorize all had their root in Euclid.
Similarly, anyone who wants to go anywhere with calculus should at least try to understand the proof of the existence of limits, at least for a few minutes, because that's what makes calculus something other than voodoo.
How can the review of proof generated by computer by a human be considered "peer" review?
Why not have it verrified by other computers?
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?
Was that just an intentionally terrible example, or did you not actaully understand a good portion of the book?
Shitram Brown, PhD
Professor of Mathematics
A fairly basic example: several centuries passed between Newton and Leibniz introducing derivatives and Cauchy and Weierstraß arriving at the formulation that's taught in high schools nowadays (at least where I live): epsilon-delta definition of the limit and going from there. Today, this stuff and the accompanying proofs look pretty simple (and they are), but without the right formalism/mental model, playing with infinitesimal quantities is somewhat of a black art. It took a long time to get there, and computers wouldn't have helped much.
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.
Russel and Whitehead's work in Principia Mathematica, amplified by the Hilbert Programme.
Godel exploded that little lot by showing how
any formal system powerful enough to represent
anything worthwhile was powerful enough to
contain contradictions.
Even simple `proof' like n-satisfiability or
showing that a string is a member of a language
defined by a context-free grammar is NP complete.
ian
For exploration, they are also useful. New series for p have been conjectured (and proved by hand) based on computer programs which search for certain sorts of integer relations. This has led to the ability to find the nth hexadecimal digit of p without finding the previous n-1 digits, something that could have been exceedingly difficult without this computer program.
With regard to things like the proof of the 4 colour theorem using computers, there is a more interesting debate here. I'm going to make an analogy with a similar debate in neuroscience which is quite interesting. David Marr, who was a researcher into visual systems in the brain, made a distinction between Type 1 and Type 2 theories. A Type 1 theory is, broadly, one in which there are nice formulas like you get in physics or maths. A Type 2 theory is essentially computational. For example, many models of the way the brain work use PDP (parallel distributed processing, a sort of computer model of neurons in the brain). Marr's point was that in general we should prefer Type 1 theories, because they give us a general and intuitive understanding of how the thing being studied works. For example, there are certain cells in the visual system which detect edges in the visual field. So, if you have a theory of vision which involves certain cells finding the edges in the visual field then that gives you a better understanding than some sort of computation model which performs the function of the visual system but which you don't really understand. However, he also pointed out that since animals evolved and were not designed, there may not always be a Type 1 theory explaining why, in an abstract general way, the brain (or any other bit of the body) worked, it just does.
Returning to maths, I think the analogy is that a Type 1 theory is one which can be completely understood by a single individual by working through it line by line, whereas a Type 2 theory might involve a computer proof like in the 4 colour theorem. In general, we prefer to get proofs which don't use computers, because they might give us an intuitive insight into why the theorem is true, or it might lead to an interesting new branch of maths (like the Taniyama-Shimura conjecture that Wiles proved). However, there might be some theorems which just do not have proofs which a single person could read and fully understand. The 4 colour theorem might be just such an example. It would be foolish to discount any such theorems a priori, and so I would advocate a cautious use of computers in mathematical proof. The danger in overusing computers is that if they become too widely used, people will search for computer proofs without finding the insightful way of solving the problem which doesn't use a computer. The danger in not using them enough is that huge amounts of effort could be wasted trying to find neat analytical solutions to problems which are not really amenable to traditional methods (not using a computer) of attack.
I'd pay $500,000 for a program that can prove the Riemann Hypothesis.
Proofs where no one understands the proof are of little use. Yes they allow you to work with the statement that was proven, but you don't garner anything from the proof itself.
Many nice and elegant proofs are just that because they are not only aesthetically pleasing, they also give their readers insight into other problems.
As Erdos used to say, they come straight from the SF's book. (if you don't know what that means, go read about him)
The end of mathematical proofs by humans? I think I speak for the entire high school populus by saying "Thank God!"
I loved doing proofs in my High School math classes. I even had my own book of axioms, thereby cementing my destiny to be reading /. someday. I didn't become a mathematician, but the merger of logic and creativity was so appealing. I wish I had been able to take it further, but unfortunatly calculus came along and whipped my but, so instead of an engineer, I became a programmer. Go figure.
THIS SPACE FOR RENT
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.
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
Actually, it was never thought to be obvious that parallel lines could never meet. Euclid tried to get rid of the postulate, and mathematicians for centuries after tried to show that the postulate was dependent on the others (the other postulates were never controversial in the same sense). In the qwest for a fundament for the parallel postulate, it was shown that the postulate is independent of the others. Then Gauss and others showed that very interesting new geometries could be created if you changed the parallel postulate with other postulates. And the story of the troublesome postulate in a way ends in the great breakthrough of Riemann geometry and the general relativity in physics it made possible. Penrose should know, he is an expert in general relativity.
Newton was challenged by among other Leibniz when Newton made time something that flows with a steady flow and that is just something physics has to accept similiarly to the existence of an unmovable space (Newton was making the concept undefinedable axioms of physics in a way). Leibniz did not like it and it lead to many philosphical debates, while physicist were usually happy to leave time as undefined since Newton's physics was so successful to explain things.
--- guns don't kill people, people with guns kill people ---
Being at least tangentially in the field of theorem proving, I can say that this is completely ridiculous. Replacing human proofs is not going to be possible until we at least have mechanical provers which can really do induction. Many cannot do it at all, none can do it well. Furthermore, quantifier heuristics are often shaky at best. This is the wall that the software verification community has been hitting for years.
----- "Type theory is like pretzels on crack." -- random friend
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/
...you would also need a bunch of biologists that can tell you exactly how the brain works, and a group of computer programmers that can translate that into code. Also remember that a brain is a living organism where the neural pathways are changing. In a computer, you must either connect all-to-all, or have a computer that can rewrite its own data paths.
Kjella
Live today, because you never know what tomorrow brings
The talk was actually about why it doesn't have to be the case that really large numbers must satisfy the same rules as smaller computable numbers. This is based on Godel's proof that says something about it being impossible to know whether an axiomatic system is free of contradictions.
Anyway, he also touched on computer proofs. He was basically saying that (most) mathematicians do what they do because they enjoy creating and understanding logical structures. To some extent you neither create nor understand a computer proof and so it is intrinsically less interesting to a mathematician. Since the world of mathematics is driven mainly by what they find interesting, computer proofs haven't featured very highly in it.
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 contradictory as it may sound, there is always a notion of "belief" in a proof. "Proving" essentially menas "persuading everyone that something is true" and the only difference between mathematics and other sciences is that the former constructs everything from very elementary axioms using basic induction rules, so that it is (usually) clear that a proof is correct.
:)
However it is common to use deduction rules incorrectly, theorems without meeting all preconditions, etc. When a proof becomes complicated, doubts arise.
But that's exactly why we can have much more faith in computer proofs. A computer can only use very specific proof techniques, written formally in some kind of logic. All theorems must also be given very precisely. And the proof can be also checked mechanically, possibly using different software to avoid bugs etc. Size is irrelevent, as long as the basic proof technique is rock solid.
On the other hand machines are stupid, you need humans to program them and prove the correctness of every proof technique they use.
PS. Reading this article was very interesting, given that I'm currently attending a computer science conference (ETAPS) one of the main topics of which is logic and computer proofs
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.
This is in regular human talk. It's not a true proof.
Imagine that you have a map that has five colors where every color is touching every other color.
It's on a piece of paper beneath a coffee can.
One color must be on the edge. There may be only one color, or there may be many, but at least one will exist.
Move the coffee can until you see that color. Lets say red.
Now imagine taking a marker and covering the rest of the page in red. (Alternatively, stretching the red area around the rest of the page).
Now you have four colors who are all touching one another, and who are all touching the outer red page.
Imagine that you have a tetrahedron. This is a 3D shape which has four sides. Imagine that each side of the tetrahedron has a color. Say, green, white, blue, and yellow.
Imagine that you poke a hole in the tetrahedron and spread it out flat - placing it on the red piece of paper.
No matter where you poke the hole, all four sides will touch one another.
However, you must poke a hole so that all four colors are on the border, i.e. so that they all touch the red paper.
Look a the green side. All of the sides are equivalent.
If you poke a hole in one of the corners, the opposite side will be in the center when you lay it down, and it won't touch the red. It won't work.
If you poke a hole on one of the edges, it's even worse. Two of the opposite sides will be in the center, and neither will touch the red. Again, it won't work.
Worst of all, if you poke a hole directly in the center of the green side. Then all three other sides will be in the center when you lay down the tetrahedron and none of them will touch the red. That won't work either.
Therefore, there's no way to poke a hole such that all four sides will touch the red when the tetrahedron is laid down, so it was impossible to have a map with 5 colors, all of which were touching one another, in the first place.
Came up with this in 1990. Never formalized it mathematically. It may not be a proof, but it makes logical sense to me.
doug@dougdante.com
The world will not get better through technology. We must seek to be better people.
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.
...but it's old hat now. Seriously, we're actually coming up on the 30th anniversary of the Haken-Appel proof of the four-color theorem, the FSG classification has been around for quite a while now, and from my perspective most of the people fretting about the nature of proof these days are philosophers, not mathematicians. Most of the serious (and many of the amateur) mathematicians I know consider the computer an essential part of their toolbox; Mathematica never accidentally flips a sign while it's going through two pages of calculations for you. There are even journals devoted to computer-aided mathematical exploration: Experimental Mathematics is more than a decade old now.
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.