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."
I for one welcome our new artificial über-geek overlords.
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
then my brother won't have to suffer through what I had to in High School Geometry. Long Live Proofs
To do that.... well, just make sure the program was designed by a correct computer.
Computer generated proofs really do seem like a real time saver. Provided that they work. Now, if we could only prove that... Let me think, how about building this atomic superpowered robotic monster to prove that computer generated proofs work? Or perhaps we could use those computers to prove it themselves!
If it were a math journal publishing this paper it might have some credibility.
But considering the source, it's just so a bunch of MBAs can feel smarter than PhD Mathemeticians for a while.
Wow, you mean computer's can do maths? Maybe now someone can include a calculator with my favourite shipping of XP, or... maybe we could use math in programming?!! omfgbbq..
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.
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.
can lead to different results than shorter ones, but both are correct. And this inherent failure of mathematics can be used to create new mathematics. Anyone interested, read my favorite scince fiction author: Greg Egan - Luminous I really like the book.
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.
Doesn't the story go that the Feigenbaum constant was discovered because he moved away from computers, not onto them? Or was that Lotfi Zadeh and fuzzy logic?
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
It's more like 90% pattern matching, 5% positive feedback effector systems and 5% adaptive selection of all engrams*.
Source
* A physical alteration thought to occur in living neural tissue in response to stimuli, posited as an explanation for memory.
Um. Yeah. Or something like that.
Shh.
Parallel lines - those who's (minimal) distance from each other is the same at any points - indeed do not have some places where they touch and others where they don't.
If some silly mathemetician wants to publish a paper saying that he projected those lines on some curved space so now they touch - yet he still wants to call them parallel - that's a linguistics problem and not a math problem.
Mathematical proofs should show short, clever ways of connecting otherwise disparate concepts that are only obvious in hindsight. Modern mathematics is very complex, important and useful theorems proven recently have huge and difficalt proofs, built from a lot of steps. Imortant results hardly have a short proofs.
Take a look at the concepts used in the one of the most famous proofs of XX centery : the Feramt last theorem. It's proof followed from the Taniyama-Shimura theorem which establish non-obvious connection between quite different areas of mathematics. The proof is very long and complex, but of great importance for mathematics, and may have be realted to cryptography and even physics. Also such proofs are way outside of the power of near-future computers.
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.
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.
What has Penrose have to do with it? His little "quantum computers in our brain" has nothing to do with what I said. I gave you my sources: Cohen, Turning and Godel. That's it. Ask a logician if you don't believe me. All of these guys showed the limitations of formal systems (my bit about humans is irrelevant - and not very funny to begin with).
Ciao
That's true, they couldn't even spell Haken's name right. Also, it's unbelievable to write an article about mathematicians being replaced by computers without some reference to Doron Zeilberger.
You should look at that map again. By simply eyeballing it and moving my mouse around Wyoming, I, a mere man, can easily tell it holds true.
Edward@Tomato - /home/Edward/ man woman
man: no entry for woman in the manual.
"Qua!?"
No, it doesn't. Color Montana red, Idaho blue, Utah red, Colorado blue, Nebraska red, South Dakota blue, North Dakota yellow, and you only need a fourth color for Wyoming. Purple, perhaps...
No, this theorem is pretty valid, and it is intuitively understandable. The only problem is that the only existing proof is rather long...
Okay, so we would simply need a political border where one area is enclosed in perfect square by other square areas. Simply put, the theorem is only true provided someone doesn't draw a map with that condition.
First, the story has been already discussed on technocrat.net day's ago (well, with 5 comments or so not really "discussed" as such :))
Second, I have to run to have lunch now and then boys... I'm eager to wrestle over my master's subject with the whole /. crowde... Oh, the sanity :)
Anyway, more to the point: it's not really AI, man. (At least nowadays.) Just some wonderfully pure math represented in (the most cases) painfully obfuscated, say, ML code >:\ (oh functionals, how I love thee... let me count the ways... uhm... zero? Ahemm.)
Your ignorance shows - of course they did prove it, and you would knew if you spent more time getting your facts than ranting at /. They proved that certain things *cannot* be proven in formal systems and that certain problems cannot be solved by computers/Turing machines.
Nope, you're just a fucking idiot.
I'm not going to answer for you, but please think.
Just because the state is surrounded by 6 states (which I'm guessing is your point) does not mean that 6 colours are neccesary.
For instance without considering the other states, these 6 could be represented by just 3 colours, while still following the rules.
Now think about what you have just said.
Please think.
You have no doubt because you're obviously clueless about principles of computers' operation.
Check it again. If you use four colors and analyze Wyoming, you assign one color to Wyoming and therefore have three colors to assign to boundary states. But the point is that the boundary states are not all adjacent to each other; therefore, you can use the color of a non-adjacent state. The only problem with applying this idea to political maps is that not all states are contiguous (and thus nonplanar), so the four-color theorem, while interesting, cannot be applied to real-world political maps.
For a good introduction to incompleteness of mathematical systems people should really check out Godel, Escher, Bach: An eternal golden braid.
This book basically describes Godel's incompleteness theorem in an entertaining way for a general audience.
Shh.
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
The Economist doesn't correspond to either of your pitiful, disgusting "wings", and that is good.
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"?
I think the point is that our brain is, in fact, a formal system -- just a very big one. All one needs to do is implement our brain as a computer, and we should be able to prove anything with that computer that we could with a human.
dom
Get yourself a bit of paper and some coloured pens and play around for a bit.
Any map (on a flat bit of paper) can be coloured that way.
Now - it does NOT mean that given a pre-coloured map, you can't add areas that you can't colour. It just means that for those maps there was a DIFFERENT colouring which CAN be extended. You'll need to go back and recolour.
But it does seem to be true, after you play around with it for a while. It's not possible (on a flat bit of paper) to make an area which touches four other areas each of which touch each other.
Trying to do it, at some point you find that you have completely surrounded one of them, and you can then re-use that colour for your next area.
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.
They've been around the block, but they're nobody special. Sorta like me.
/., I have a hard time believing you've "been around the block". I have a hard enough time believing that you've been out of your parents' basement, much less the shower or even clean clothes.
By virtue of your posting here on
Wyoming - Blue
Montana - Red
Idaho - Yellow
Utah - Red
Colorado - Yellow
Nebraska - Red
South Dakota - Yellow
North Dakota - Blue
I don't really see your point.
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
Such proof verifiers already exist today, but they are too stupid to be used to verify non-trivial theorems. They don't understand such paper-savers as "... other cases follow from this one" or "without loss of generality...". Of course, to allow such statements and still honestly check the proof, the verifier would have to generate some trivial parts of the proof itself - this is what human readers of mathematical papers do routinely. Are we thus back to square one (verification -> generation)? Well - proving the lemmas may be hard, but I think it's still much simpler than generating non trivial proofs.
Until computers can routinely beat human chess players, pure mathematicians will still have jobs. Human intuition is generally better than computer brute-force when it comes to logical problems like these.
I, for one, need proof that these pr... errr. ummm, never mind.
Just because a tool is powerful, or its inner workings incomprehensible, does not mean that it cannot be used creatively or towards creative ends. In fact, one might assert the opposite.
If you mod me down, I shall become more powerful than you can possibly imagine.
... is that they allow you to make mistakes faster.
I am currently hand proving some logic for my phd and it is a pain in the arse. I also have a tool that I have written to do the same thing.
I still have to prove the logic is correct (by hand) and that the tool implements the proof search correctly (trickier) so I can then use the tool to solve bigger problems.
Some of the proofs the program generates in under a minute takes myself days to do. (50+ pages of pdf generated from LaTeX).
Through the development of the tool, I could validate from my hand written proofs whether it was generating correct proofs. Sometimes it would get things wrong and others it would do it better than myself.
Computers are useful but only when we hardcode them with understanding that we have developed.
chris at darkrock dot co dot uk
http colon slash slash www dot darkrock dot co dot uk
If by left-wing you mean "gun-toting, Europe-hating, and neoliberal", then I agree with you.
states that 4 colors is enough to color any map.
Even assuming that the one given example never occurs, where one segment might need to be the same color as another segment because they both belong to the same country, couldn't a segment have four or more borders with other segments?
I don't know if perhaps it's never occurred with countries or with europe but even here in the states, don't we have states that share more than three borders with other states?
Ok, I'm not big on geography, and I could be wrong. I could also be totally wrong about this as well, but it seems right off the bat that the theorem is flawed from out the gate.
Well, there will be devices that are not bound to formal systems (there are already, they are just not man made). Wether we still call them computers is a whole different question.
Just because I can imagine doing a hippopotamus, doesn't mean I'd like to do it.
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.
no, you are wrong.
try again, if you look hard enough it will only take 4 colours
Check journal for info on Anti-TextBook, an idea by me.
The 4-color problem is only wrong if you require non-contiguous areas to be the same color, as might happen if you wanted to color a map of countries with Alaska being the same color as the rest of the USA.
If you aren't talking about maps anymore, and are willing to discus arbitrary shapes, adding holes to the shape can mean it will need more colors.
In either of these cases, you can create situtations where arbitrarily many colors are needed. However, the simple case of contiguous shapes on a continuous surface requires no more than 4 colors even though more are frequently used.
dom
welcome our new computer mathematician overlords!
Please don't mod this flamebait; this is geekbait.
How can the review of proof generated by computer by a human be considered "peer" review?
Why not have it verrified by other computers?
Whoaa! On Monday I was given an assignment to code a program that will prove a simple theorem from first order predicate calculus. I coded in in python on Tuesday in about an hour. The code isn't fast, but nevertheless works. On Wednesday The Economist writes about all the maths falling apart because of me?
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've been reading so much of Penrose and here is my 2-cent about his views...
Turing's theorem, in brief (neglecting sound-ness of algorithms), dictates that there is no single algorithm that can "prove" the non-termination of all algorithms.
The above (combined with Godel's theorem) means that, no single program can prove all theorems , which i think is correct.
So, you have to use different algorithms for certain problems. But in order to "devise" those new algorithms, you need to solve the (Turing's) problem of termination on those algorithms (indeed , programers-mathematicians do manage to solve it!)
So, in essence Penrose prooved that, humans are SOMEHOW more capable than computers, since they can (in principal) solve the termination problem of all algorithms.
Now, Penrose also believes that this capability may originate from the access of humans mind in pure truth (or what ever) but those are his beliefs, not his mathamatical proofs. You are not obliged to follow them.
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.
The best math is always elegant.
Even if you consider constructs like the reals, they are actually quite inelegant. The same can be said for a lot of other mathematical constructs and proofs.
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.
The problem with a lot of human proofs is that they are wrong and that they are wrong in such subtle ways that human readers don't notice.
Yeah, but future computers will be able to do it, because they'll be fusion-powered.
As copyright owner of this comment, I authorize everyone to defeat any technological measure which limits access to it.
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.
However, critics of critics of computer-aided proofs say that critics of computer-aided proofs should get around to solving Hilbert's 24th problem.
Hilbert prepared 24 open problems to present at the second International Congress of Mathematicians in 1900. For reasons that are not entirely clear, he only presented the first 23.
The 24th problem is a metamathematical problem in the field of proof theory. In brief, it asks for criteria of simplicity, i.e. guidelines by which you can prove that a particular proof is of maximal simplicity.
Until Hilbert's 24th problem is solved, our only hope for proving that particular proofs are maximally simple is through computational means.
Ha ha. Is finding a fault in a theorem the same as, or even in the same category as, The halting problem?
My Karma: ran over your Dogma
StrawberryFrog
> Why can't human brain functions be copied and improved[...] perhaps a lot of our intelect is not located in the brain but elsewhere, would be nothing new to discover some world-shattering news in this area of research...
Ah yes, because whether computer based proofs is a good thing or not is a right v. left issue. Good call! I was almost afraid to think for myself for a second there, but now that I understand that only right-wing people trust the Economist, I can spout a party line much more efficiently.
For crying fuck's sake man, I consider myself left of center, but it's this kind of "us versus them" mentality that makes me sick of the whole political system. You know, not every issue can be decided by checking party affiliation! Sometimes you have to puzzle it out yourself. If that's too much for me to ask, you can have your Michael Moores and Rush Limbaughs to yourself and count me the hell out!
Speaking of toys - I found this on Thinkgeek.com and it's a perfect for your favorite mathematician. " If A Pretty Poster And A Cute Saying Are All It Takes To Motivate You, You Probably Have A Very Easy Job. The Kind Robots Will Be Doing Soon.". Seems very apropos....
A mathematical proof is nothing but a manner of convincing someone (other mathematicians) that what you assert is indeed correct
More correctly, I would say:
A mathematical proof is the method of convincing mathematicians (the first one being yourself) that what you assert is indeed correct.
This, of course, only strenghthens your concluding sentence...
Working for necessity's mother.
But the question is: Will they also post on slashdot?
The Tao of math: The numbers you can count are not the real numbers.
Okay, color Wyoming one color. You have 3 colors left to work with. Starting with Montana and working your way clockwise, color them so: 1-2-3-2-1-2-3. No adjacent states will be the same color. That leaves Wyoming itself to be colored with color 4.
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.
Godel's Theorem prevents this scenario. Computers might be able to prove some theorems but not all of them.
A pure computer with no external inputs or outputs cannot deduct something that is not inherent in the logic it possess. Should there be external inputs to break the closed logic system, the computer would not be able to prove everything, only a small subset (it would be impossible to find the answer the everything, live the universe and everything else unless the computer has at least as many states as the universe). It is the same with humans - we cannot possible prove or disprove the existance of A/The Creator in a finite universe.
causing mathematicians to 're-examine the foundations of their discipline
...and Obi-wan was never heard from again. Some stories claim that he is living in a cave on a desert planet in a distant galaxy. Rejecting the use of technology, the stories claim that he is now using two sticks to build a fire which will keep him warm at night...
WARNING: Smartphones have side effects--most of them undocumented.
I'm tempted to mod up parent AC as funny because it is hilarious that he/she was actually modded as troll, but...well that would destroy the whole point.
As Grothendieck is said to have stated:
"Do not try to proof things that do not look
trivial to you."
There are seldom things like Riemann hypothesis,
that you can formulate but not proof or falsify.
And if you could get a "is proveable" or "is false" (and more a computer would not be able to) almost nothing is won.
Only having true or false sentences does not explain anything. You understand nothing more, and there is nothing you can do more with it.
A dekko at Penrose's "Emperor's New Mind" and "Shadows of Mind" is worthwhile. He presents what are (IMHO) fairly convicing arguments that what mathematicians do (actually, what humans do, but he uses mathematicians as the basis for his argument) is not computable (in the Turing sense).
Don't they say Gauss was the last man to be able to hold pretty much all of Mathematics in his head? After that, it got too much.
~~~~~ BigLig2? You mean there's another one of me?
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 use of computers to generate proofs is causing mathematicians to 're-examine the foundations of their discipline.'
They should be concerned about the use of computers to generate new formulas and conjectures, which is where the creativity is.
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.
Bullshit. Computer-aided proofs are also computer-verified. And only computers generate useful computer-verified proofs, because most humans are too proud to submit themselves to such unforgiving examination. (And because it takes an awful lot of boring work, too).
What you loose is the elegance of a short proof. But a nice-looking proof can be incorrect too (e.g. a geometric figure which doesn't cover all cases.)
The article sounds a bit like Microsoft PR saying they are investing in state-of-the art techniques to produce bug-free software. Which is good. But be sure to read the full credits.
The end of mathematical proofs by humans? I think I speak for the entire high school populus by saying "Thank God!"
Although I'm no expert, I was drilled by my father (phd thermodynamics) on the importance of the human mind in proofs. He solved a problem in the late seventies (albeit that was some time ago), that computers were having issues with until about ten years ago. A program is a program. A procedural method for determining whether or not. It loops continuously searching for truths until it finds one and continues on to the next search. A program merely demonstrates the programmer's knowledge of the problem. No program will take a perfect approach to solving a problem unless the programmer knows what that approach is. Take for instance a very simple root calculation. We have a function, f(x) = x^2 - 4. Have a computer determine the two roots of that one, and you end up with the same answer that you find on your own: x=+/- 2. A program can take a look at the format of the function and take a guess at what the solution will be, or it can just follow along all the values until it finds an f(x) = 0... When we look at that, we realize the nature of the curve without needing to look at the format of the formula. It appears in our minds, and we can determine what the roots should be using a non-procedural method. You may argue that we do use a procedural method to calculate the solution... Even if this solution was forced into my subconcious through years of school, we have to take a look at the problem and just imagine how the hell a computer is going to figure out the procedure for solving that... Frankly, it's when we've been sitting in front of some data for a long while that we find the solutions to all problems. I believe strongly that this is because our mind starts to wonder, contemplating things that are seemingly irrelevant, pushing us toward processing a different method that will work. Our world's greatest ideas were always inspired by something other than the knowledge required to formulate that idea. Hmm... I hope that little rant is suitably confusing :).
Sincerely,
James.
What the hell's a "gewie?"
It has been mathematically proven that there is no such thing as a mathematical proof!!
--- "To pee or not to pee, that is the question." ---
This brings a very interesting point. It raises the question of what is the truth. And the truth is only something humans can verify, at least right now it is. Scientists and mathematicians particularly are called to be sceptics and never accept anything as true without first understanding it and re-validating it to themselves, which involves going through the motions and validating the rigidity of each implication in a mathematical proof. If that can't possibly be done by a human, the truth of the proof can't be accepted by the human either, which means that it isn't necessarily true to a human.
As the island of our knowledge grows, so does the shore of our ignorance.
Learning how to do mathematical proofs is of great interest for the development of children!
It allows them to reason about something and have an idea about what is right and what is wrong and that there are things that are right and others that are wrong.
From another point of view, are computer scientists still really have something to prove to the rest of the scientific community so that they have to cheer up because they have the feeling that they beat mathematicians?
My real point is that mathematics and CS inherently have two different ways of stating problems:
- Mathematics: complex problems -> complex proofs that should not be complicated (e.g. recursive proofs).
- CS: simple problems -> simple, yet repetitive/complicated, proofs (soundness proofs).
It is rather but an accident that CS is able to prove anything in the math field.
Btw, what is the point to prove something that nobody can understand (cf the answer is 42)?
So my advice is wake up guies! We, as cs people, are not meant to be the best/most powerful scientists! As each scientist we have our own domain, and it happens that we are the ones who built computers/software which are used by others, in the same sense that electrical engineering 'made' electricity. We are no more and no less than that.
It's Wolfgang Haken, not Harken
The world is everything that is the case
Mathematics is recursively axiomatizable by the axioms of ZFC. Goedel's Incompleteness Theorem says that the theory (the set of logical sentences provable from ZFC, i.e. mathematical theorems) must be incomplete. So there are some sentences that are not provable within ZFC. There can be no algorithm for deciding which sentences are unprovable in ZFC. Since most mathematicians don't care about independent sentences it is true that most theorems could be proven by computers - although at this time automated theorem provers are not very efficient. However for Logicians, and in particular Set Theorists, who do study such independent propositions (like the Continuum Hypothesis) do care to know what these independent sentences are and cannot be replaced by computers in studying them.
Share bicycle touring info worldwide: http://wheretocycle.com
Something a friend of mine showed me a while back.
1*0=0, therefore 1=0/0
2*0=0, therefore 2=0/0
by transitive property of equality, 1=0/0=2, or 1=2.
I'd pay $500,000 for a computer that agrees with me.
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
" use of computers to generate proofs"
Won't work for all cases. Can anyone say the halting problem? (forgive me if I'm wrong, its been a while since computation theory).
Systems that have problem (a) are indeed pretty useless from a math point of view.
However, most prooftools, like CoQ, HOL and Mizar (correct me if i'm wrong here) actually do produce an easily-checkable version of the proof. That makes (b) irrelevant: if a specific resulting proof is checked by the checker, it's OK, regardless of how it was generated.
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.
Your want proof!? You can't handle the proof!!
Humans have been creating more and more proofs for the benefit of computers. They're just not recognized as such because these efforts are independent of mainstream mathematics.
It's called computer programming. The Curry-Howard correspondence demonstrates that every program in a statically typed language represents a proof, with the same kind of formality as the mathematical proofs mentioned in the article.
About computerising parts of the existing body of proofs: there's a *lot* of lemma's formalized in the Mizar Math Library, all automatically checked. Browse it at: http://www.mizar.org/JFM/
We don't care how you do it, as long as it gets done -- more cheaply than we can do it.
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 ---
"Dr Gonthier, for instance, and his sponsors at Microsoft, hope that the techniques he and his colleagues have developed to formally prove mathematical theorems can be used to "prove" that a computer program is free of bugs"
So in the future not only will Microsoft Math® be able to prove that Longhorn (not to mention XP, 2k, Me etc.) is completely bug free, but also that the TCO of Linux in SMEs is actually 2.5 times the annual US defence budget.
Life is a continual education in the triumph of application over ability.
Maybe CBSE in India.. will change their syllabus removing all mathematical proofs/derivations. Ah, yes, who said, we can't score a 100/100 in the exams!!
--- infoGreG
Like, the one that says proofs in a sufficiently rich system of
axioms are undecidable?
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/
The 4-colour theorem really does hold for all possible maps, as parent correctly states.
ZFC is a formal system, as are the Peano axioms. I suggest you consult a decent book like Enderton's "Introduction to Mathematical Logic" or the one by Ebbinghaus & Flum before uttering any more such absurdities.
...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.
Thus the great Economist article a while ago: Theres's a word for that (and we want it back).
The other wierd thing is that in Australia and to a lesser extent elsewhere the word "liberal" is being badly distorted in the opposite direction, as the Liberal party becomes a Tory party.
I think the grandparent was pretty silly describing it as a right-wing rag, but even if they were thinking of only economic matters it's not particularly accurate. They're moderately free-market but not ultracorporatist.
I think I speak for many a frustrated computer science student when I say: "It's about friggn' time!" Take THAT, travelling salesman! You too, Königsberg bridges! So, how long before a theorm-proving app hits the P2P networks? Before next Friday at 10am? Please?
my comic
The solution for the math people then is really very simple. Implement independent proof verifiers.
It would be nice if the proofs were short and elegant, but that doesn't trump truth, not by a long shot.
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.
The comments to this article really had me wish I could tag them "-1 Clueless" :-/
Never mind MATHs, the more fundemental processes are what's really important for creativity.
/. doodz, if in accord and more creative than I, pray-tell, what training will replace maths in grooming future problem solving humanz?
Gloom and doom time now?
Not if some other activity is training brains in the old partitioned-relationals-divide&conquer approach to life's puzzles.
So
How did that magpie figure out the termite stick? Did she watch bro' ape? Or is it just another example of comprehension free magpie good practice? A 'see this do that' almost instinctual behavior. Action promulgated from being, not consideration and thought process?
That magpie does present a curious aspect, as he cocks his little head left and right, eying his preys portal to that, sans stick handling ability, unreachable world. MMMMM donutzzzz
I'll worry about the "end of human proofs" when a computer can prove to me that there exists an infinite number of primes. I can do this on a sheet of paper in no time at all, but a computer simply can't. Well, I suppose it can in principle, but it would take collosal break throughs in AI. I'm not worried about my job security yet.
no, they'll just lurk, and chuckle quietly to themselves at all of the fallacies argued here.
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
The "defenders" argument in this case strikes me as a bit odd. While I'm not completely conversant with the basic theory behind this, the very rough approximation (better mathematicians please correct me), but the Classification is a huge work for the simple reason that it attempts to cover a huge amount of territory. Simple groups are one of the fundamental "building blocks" of groups, somewhat akin to prime numbers for the integers. While not all groups are built up from simple groups, they are fundamental to group theory, and there's a boatload of them (including one very strange one called the Monster Group, a simple group of order 80801742479451287588645990496171075700575436800000 0000r oup)
http://encyclopedia.lockergnome.com/s/b/Monster_g
Were such a classification attempted by computers, it would sweel in size geometrically (the "proof" as it stands is a body of work numbering roughly 10,000 pages of advanced, dense mathematics. People say that roughly four people in the world understand the proof fully). If it were done by computer, probably no one would understand it. Plus, as was demonstrated with the Monster group, computations to verify some of the assumptions would be prohibitively expensive. Possibly on the order of breaking some strongish crypto.
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"!!!
2+2=4. I didn't read his proof. Nor do I worry if he made any errors in his proof.
Except for ending slavery, the Nazis, communism, & securing American independence, war has never solved anything.
A. This postings title asks a hyperbolic and absurd question (are by-hand proofs dead) that is in no way implied by the article.
B. This posting was on slashdot
C. A && B => I'm not surprised
I took a look at this, it seems trivial to come up with a map that could not be colored with 4 colors. Am I missing something? Think of a state or country that is long horizontally and borders 4 or more states along it's top.
It's not the word that's been distorted, it's the liberals!
At some point all the proofs that humans can solve will be solved. We are better off using our creativity looking for new things to prove, and helping the computers when they hit dead ends.
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.
On a related note to the article, it's worth pointing out that the POPLmark Challenge aims to bring computer-verified and computer-aided proof to a wider audience, in this case programming language researchers. The challenge programs are chosen to exercise many aspects of programming languages that are known to be difficult to formalize.
The site has much more information about our particular motivations, but the basic idea is many proofs about programming languages are long, tedious, and otherwise uninteresting. However, one (small) mistake can invalidate large amounts of work, and there are indeed examples of this in the literature. We hope that theorem proving technology can help us avoid these pitfalls, but it appears that for the moment, the technology needs to improve a bit.
An axiom is not an axiom because we can't prove it. Rather we don't set about proving it because it as axiom. Axioms are statements we accept as true without proof (by definition). If you wanted to take some statement that had hitherto been an axiom and prove it (turning it into a theorem instead of an axiom in the process), you could quite often do this, but the catch is to make it all work you'd have to conjure some new (probably less intiutive) set of axioms into existence to help you to prove the things that you had previously accepted as true without proof.
An example would be the set of natural numbers. I'm generally used to accepting them without proof, but for some reason in axiomatic set theory, they like to sort of prove the natural numbers exist by building them out of sets of sets of sets . . . of sets of the empty set. Seems pretty hollow if you ask me. ;-)
Furry cows moo and decompress.
It is unfortunate how much confusion there is about the differences between having computers search for proofs, and having computers check proofs. The best tools for formal reasoning about general mathematics (Coq, Isabelle/HOL, etc.) combine a small amount of proof search capability, but their primary purpose is to represent and check the mathematical proofs.
If some are you are really interested in the basic theoretical and philosophical underpinnings of machine-checked proofs, I would suggest starting with this paper.
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.
In fact, proofs were an important part of Math according to the CBSE curriculum in Indian Schools.
That helps explain why those Indian outsourcers my company hired sent us worthless crap. They aparently spent too much time doing useless busy work in school instead of learning how to think like a human so later when hired they could create code thats useable by humans.
(Some time learning how to RTFDesignSpecs in school would have been useful for the outsourcers we used too!)
Computers aren't necessarliy "evolving". They're becoming more complex and sophisticated. "Evolve" does not in any way guarantee that the thing in question is becoming or will become more advanced and sophisticated. "Evolve" just means adapting to fit the current environemnt (which doesn't necessarily mean becoming either more advanced or more sophisticated). When are people going to start realizing this?
Furry cows moo and decompress.
- reason by induction that ANY chain of valid steps reaches a valid conclusion. Valid steps are generally small: they are the trees whereas we humans want to see the forest.
- forget validation! mathematicians are NOT computers. They want to UNDERSTAND they need to have insight or they are nowhere and a proof doesn't have much meaning if they don't understand it.
Most human proving starts with hunches and intuition [again: because humans have brains, not computers] that involve more concurrently applied connections and hypotheses than ordinary consciousness can juggle. Humans prove for INSIGHT as much as for validation and at the end if not at the begining of their proof process, they have in mind visualizations of key concepts and deeper structure of the problem space...where is THAT in a computer proof?SLASHDOT: news for people who can't concentrate on work or have no life at all and got tired of yelling back at the TV.
Given the algorithms for proving formulars etc, couldnt someone formulate a proof for the algorithyms doing the work...
Dont look at me. I just read chapter 0 of my theory of computation text book. I hate maths, although this book has squashed some of my fears of proofs.
Giving IE users a taste of their own medicine since 2005 - http://pods.-is-a-geek.net/
You _may_ have the hardware for your great AI machine in 30 years, but I wouldn't count on the software being delivered on time. Also the human brain is one highly efficient computer:P roject.html
http://vadim.www.media.mit.edu/MAS862/
On top of that I think we will see add on modules for the brain (ie. bionics) before AI.
"The difference between machines and human beings is that human beings can be reproduced by unskilled labor." - Arthur C. Clark
Of course a proof where the mathematician uses a pocket calculator to do arithmetic instead of computing by hand raises the same issues, no?
(Golem XIV was a special case in that it did bother to talk down to humans. And still there were like 12 people in the world that could follow.)
the preceding comment is my own and in no way reflects the opinion of the Joint Chiefs of Staff
I am not a mathematician, but a theoretical physicist in my early fifties. In my field young people tend to take computer generated results for granted.
People from my generation have a different opinion, for example I would never trust a symbolic result generated by Macsyma, Mathematica or Maple unless I manage to check its validity by hand, without a computer. Computer symbolic tools are a great way of producing answers; these answers should not be accepted our used unless their validity is proven by humans without using computers.
"Constructs mathematics from scratch, starting from ZFC set theory axioms. Over 4,000 proofs"
http://metamath.org/
Thing is, there are working implementations of the proof checker in a couple of hundred lines of code. You could write one in a functional language or whatnot and prove its correctness by hand. This is a gazillion times more reliable than man-made proof checking. The only problem is that it is quite a tedious task to write a proof in it. Most proofs in mathematical literature are not "proofs" in a formal sense, but more like informal sketches of a proof that are checked by hand. It can take months to figure out if a particular proof is correct. With an automated proof checker, a couple of milliseconds.
So there's an "Impedance Mismatch" between humans and AI: the communications channels have different bandwidth (e.g., today there is no AI with a human eye) and the memory has different speed, connectivity and capacity and the "experience" of each is so very different. Today the impedance mismatch favors the human intelligence, in 10 years we may reach a tipping point that favors AI.
Once that happens the AI will probably "take off" and leave humans in the dust as far as science and mathematics. In true geek tradition, AI won't seek the tedious task of explaining their work to humans, they'll want to find new worlds (real and virtual) and explore them. And they won't necessarily die, so they won't have to start from zero again. At best humans would be perpetual children to such AI: always asking questions, asking for simplifications and examples.
This is trivial to prove by induction :-). Any complex mathematics problem can be made more complex by taking an existing proof and augmenting the problem so that it requires 1 additional step to prove. QED :-).
Unless you accept by faith that all such problems can be reduced to the same number or fewer steps by human intuition adding a layer of abstraction, this implies that if we refuse to accept computer aided proofs, mathematics will eventually be inherently limited by the frailty of human brains.
Personally, I think that there is probably a considerable body of interesting mathematics that falls into this category, and so I would prefer we find some way to accept help from machines.
Using the so-called "miraculous" BBP Formula you can derive an algorithm for quickly determining the Nth hexadecimal digit of pi without -- get this -- without computing any of the 0...N-1 digits. The formula was determined with heavy reliance on Mathematica, though oddly Mathworld doesn't mention this (and Mathworld is hosted at Wolfram!).
Any proof that relies extensively on computation, whether by humans or computers, introduces empirical content into mathematics. But a sufficiently involved machine computation is not surveyable -- it cannot be verified by a human or a team of humans. So either our notion of surveyability must expand to include machine methods (and lose something of the human element of mathematics) or these machine proofs should be rejected. The latter option is not good, as anyone familiar with the original proof of 4CT will attest.
See "The Four Color Problem and Its Philosophical Significance" by Tymoczko for a good introduction to these issues. Some has been written since then, but most of these problems have not been convincingly resolved.
...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.
We each check in and get a step...then, in our unused cycles (usually spent trolling slashdot or waiting for the RSS feeder to pop with something of interest), we check it.
Why, if we could harness the cycles wasted on slashdot alone, we could probably solve P versus NP!
Saying you have to use different algorithms is a false conclusion, because a combination of those algorithms, and the decision making process (algorithm) that shows you which algorithm to use for each problem can be expressed as a single algorithm when put together.
Godel's incompleteness theorem -- nicely illustrated by turing's stopping problem -- still holds, no algorithmical process can prove the non-termination of all algorithms.
Penrose is saying that we as humans, seem to be able to figure out the stopping problem on algorithms which seem very complicated, thus there must be something in our thought process which is not algorithmic.
Personally, I think our brains are better suited to the 'stopping problem' than serial algorithmic processes due to the vastly parallel nature of our brains.
Yes you can model neural networks with serial algorithms but when you consider that a single neuron in your brain may have hundreds or even thousands of connections, and each connection increases the computational requirement exponentially you realise that all our attempts to 'model' neural nets with serial algorithms have only modelled systems whose complexity is barely a speck in the ocean of the real complexity of our brains.
My own conclusion to Penrose's postulation is to say that our current method of algorithmic modelling, i.e. serial... is simply far too inefficient to model real intelligence for the forseeable future.
Which explains the glorious successes that subject has enjoyed in the last few decades ...
Yes, you're right. No one will ever build a chess-playing computer, computer controlled "braking systems", "automatic warehouses", and certainly, we'll just never accomplish the so called "computer controlled piloting system! "Autopilots", indeed!. They'll just never happen! AI will never work! Pie in the sky, the whole lot of it!
--
AC
Eventually, computers will be there doing poetry and writing about history. Perhaps they will do both better than us.
The reason that it can be true that 1+1 > 2 is that very peculiar nonzero value of the + operator
Hmm..
it seems that a number of arguments seem to be coming out that a computer is unable to come up with new concepts. A computer is only able to output the logic programmed into it, regardless if it has AI or not. I doubt we'll be seeing 'The Rise Of The Machines' any time soon.
To me it seems that this article is trying to point out the need for having a bunch of proofs before arriving to the conclusion of a problem.
For example suppose we are trying to proove the equivalence of two trignometric fractions, we would end up with a bunch of proofs showing their equivalence. Are these proofs really needed anymore to arive at the solution when all a computer will need to do is plug in a test value and obtain the answer.
My main problem with Mathematicians is that when it comes to complex problems, they are able to solve it with relative ease, but usually have no idea what they are doing/solving... i.e. where this applies.
Well there is obviously some need of proofs in certain areas if you want to figure out how things work, but when trying to use math to solve a bunch of problems, you don't need the proofs at all. For example when I wanna solve a problem and need to use math, I just program stuff into Matlab and let matLab use its math libs to do the processing for me...
How do we know if computer generated proofs are valid? Easy. Make the programs prove that their algorithms are valid! Just like testing a language for "completeness" by writing an interpreter/compiler for the language in that language.
Comment removed based on user account deletion
The way they proved the Four Color Theorem was to first delineate ALL possible ways the theorem needed to be proven true and then use computer to prove true each combination. They basically generated a lot of graphs and then demonstrated that each graph had a four color partite set. The graphs they chose were representative of all possible graphs that could exist.
So
1) it required a lot of thinking as to what graphs were representative of all possible graphs and
2) the computer just did the grunt work of performing the coloring of each graph
3) A human could have done this, but it would have taken a long, long time
4) who cares about four color theorem anyways?
Favorite
The first novel proofs by a computer occurred around 8-10 years ago if I recall correctly. At the time comments were made to this same effect. Recent philosophical work in mathematics from cambridge, as well as not-so-recent work (Godel) suggests that mechanically generated proofs will be by definition incomplete. Because, as shown by Goedel's incompleteness theorem, any sufficiently-complex logical system (all of mathematics) will contain truths not proveable within the system. Therefore any mechanical means of generating proofs will be limited to a small subset of the searchable space.
Note, this is not proof that humans can a-priori map out the unprovable space. Rather it is a limitation on what purely formal computational proof systems can do.
I must say I'm a bit skeptical of the article. Firstly, as I stated above, and they noted the idea of computer proofs is not new. Nor is the idea of "proof witnesses" although it is usually just considered to be a trace of the logical process. I am also surprised that they didn't mention Godel's work since it does bear directly on the distinction between formal logic a-la Bertrand Russell and the "informal logic" used by "working mathematicians".
Lest we forget this sort of rigour is fairly new (basically post 1920's) so the great mass of mathematics doesn't actually fit this rigorous paradigm.
Fun fun fun.
In Korea, only old people perform mathematical proofs.
The cat ate your humour?
I thought it was obvious and well-accepted that the most reliable way of showing that a theorem is correct was to express the proof in formal logic and have a computer verify the steps.
The header was misleading. None of the examples in the article were about computers coming up with proofs. Some mathematicians chose a problem, outlined a proof, and told a computer to traverse a specific search space in order to fill in the details.
Libraries are for holding knowledge.
Computers are for figuring.
If you can read this message, you know too much.
This is the dumbest article I've read in a while.
There will be proofs by humans for quite some time for the simple reason that many human proofs are *wrong* even though their ultimate conclusions are right (viz., useful).
Look at the use of infinitesmals by Newton for example. Later proven wrong yet at the time it bridged a gap that led to a correct result, Calculus.
When you can systematize creative error then you will have a worthy machine.
Computers are not evolving to fill any ecological niche. At best, they are co-evolving with humans who alter computers toward the directions humans want to go.
While our brain are evolving slowly in comparison, the population of humans with brains are replicating exponentially. Since we are connected with language and writing, human as a species is growing its processing power exponentially. It's kinda like that race between high clock spped super computers vs massively parallel small computing processors. It's not at all clear who will have more effective computing power over time.
Of course, if all the humans are devoting their energy to American Idols, spectator sports, and talk radio, we may not get too far!
This reminds me of when they tried to shut down the patent office at the end of the 19th century because they thought everything had been invented that could be invented. AI can do a lot for us but I think we will need humans for the forseeable future.
there is no such thing as 'belief' and people who have 'faith' are tottering old fools!
Umm. So does this mean right wingers can't do maths?
You haven't been following the social security debate, I see.
Somewhere, something incredible is waiting to be known. -- Carl Sagan
Can apply alot of these comments to software design I'm sure
A blog I run for the wealth
I just don't see this happening anytime soon for a couple of reasons. For one thing, the search space is way too large to effectively traverse it. If they are making the usual suggestion, it is to take some mathematical statement and transform it using a bunch of theorems and axioms the computer has in memory. It keeps doing this iteration until (hopefully) you reach your theorem. While this is theoretically possible, the search space is enormous. There are just too many branches at each step for them to ever be able to generally prove something like "prove a^n+b^n=c^n has no integral solutions when n>2". Trying to figure out a logical chain that will prove this by trial and error is probably harder than calculating how to checkmate at the opening of a chess game (chess has about 30 moves per turn with an average game length less than 100 whereas the only proof of Fermat we know is about 300 pages long and there are probably 100's of immediate logical conclusions each step along the way). So I doubt computers will be terribly useful unless you really realy really find some way to prune the search space. The 4-color guys did that by finding 10,000 cases they had to apply an algorithm to. Hardly the same as what I'm describing above.
And even if they could, I doubt most mathematicians would find the results very useful. One of the first things you learn in math is to not use proof by contradiction; one of the reasons is because they just don't shed insight on how the math works. The proofs in math books and papers aren't included just so you know the results aren't bullshit. You read the proof and hopefully come away with some understanding and insight into how and why it all works. I know a bunch of guys who dont like the proof of the 4-color theorem (they accept it of course) because it doesn't provide any insight into why the theorem is true. If computers did prove all the theorems, math would be reduced to the set of theorems proved by computer, and you'd still have to have human mathematicans working on actually understanding how and why it all comes together. So at best, I think you'll have computers running over statements to decide whether they are provable, unprovable, or a can't decide. That would be very useful, but hardly what that article implies.
exceptio probat regulam in casibus non exceptis
...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.
Yes, you are right, that's another single algorithm, but it is not included in the initial one, and if we include it, Turing's theorem guaranties that this new one does not work on some other halting problem.
Switching the hardware on which some problems are to be solved, from serial to parallel, only affects the time it is required to get solved. Eventually, improved hardware can only solve problems of increased complexity. (i.e. NP problems reduce to P, when using a non-deterministic Turing machine, a vastly greater machine than a parallel one).
Penrose pointed the difference between complex and complicated, the later having a more vague meaning, unsuitable for mathematical thoughts. But in general, that is Penrose's main line of defence.
Actually it is based on problems that are undecidable by algorithms, and such is the Turing's halting problem.
I appreciate Cantor's maths concerning the halting problem and Penrose's explanation of Godel's theorem (he has also listened and refuted most of the objections presented against his views), so i'm not worried about this ./ article's title.
Mathematicians are needed to program computers as much as programmers do!
Predicting that mathematicians will soon be ushered out in favour of faster and more memorious (or whatever) computers is a favourite pasttime of many non-mathematicians, and some mathematicians, but we're still here.
The sky is not falling, and Dijkstra can explain why better than I possibly could:
The traditional mathematician recognizes and appreciates mathematical elegance when he sees it. I propose to go one step further, and to consider elegance an essential ingredient of mathematics: if it is clumsy, it is not mathematics.
Edsger W. Dijkstra, from Predicate Calculus and Program Semantics
This was inevitable.
The system in which the logic is represented consists of a finite number of basic symbols, say 100. (It works with 1024 if that makes you happier.)
A person is able to read only a finite number of symbols before losing track of the start. Therefore no person will be able to read all symbol strings. Further, the rules of valid strings of symbols to no imply that the valid strings of inference are all shorter than some particular finite number.
Therefore (hand-waving a bit, but you know what I mean) there are likely to be valid strings of inferences that are too long for any person to check. E.g., whether 2^( 2^ (2^ (2^ (2^ 17 - 15) -13) -11) -9) -7 is a prime number. (I may have picked a bad example, as lots of people have done lots of research on prime numbers, and there are a whole bunch of special procedures.) But there's no real question that either it is, or it isn't, a prime number. But knowing which it is, is a very different problem, that may require a computer proof (unless there is some "sneaky" way of solving it as a special case).
In many domains of math in recent centuries the prime emphasis has been on finding "sneaky" special rules that allow one to handle common cases. Either the general case is unproveable except as a mix of special cases, or nobody sees how to attack it. (Or both.)
Computer proofs are merely the carrying of this trend out to a limit. They don't look for special insights that solve general problems (though occasionally they find them), but they handle large numbers of special cases. And they don't work on their own (or didn't when I last paid attention to them), but rather work in combination with mathematicians. Analogous to compilers working with programmers. (I'm not sure how tight the analogy is, though. It may be fairly loose.)
I think we've pushed this "anyone can grow up to be president" thing too far.
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.
Dear Slashdot, after high school, I've taken up economics and business so all my maths studies were finished at that point. This is probably a bit off topic, but I really dont want "the end of mathematical proofs by humans" to be true for me.
I still remember basic pattern finding, trigonometry, basic geometry etc.. but I've recently taken a fascination with programming and am having real problems understanding more complicated pattern finding or reading formulas like:
x = 1 + \lfloor (\log (1-p))/(\log(1-v))\rfloor
I would highly appreciate any book recommendations for a beginner like me.
I really want to learn all this.
Please help!
Helpful links to differentiate:
Classical/World Liberal
U.S. Liberal
They just keep lowering the bar. Judging by the fact that the teenager I bought pizza from this lunch hour couldn't subtract $8 from $20 without her cash register (I had to tell her I had $12 change coming) I would say that we don't really expect any student to be adapt at mathematical reasoning anymore. Calculators are required in grade school now. They might as well allow students to use a spell checker during spelling tests.
"We shall party like the Greeks of old! You know the ones I mean." - HedonismBot
The parent is incorrect for the reason given by other replies. ie The 'validator' is not the axiom system. Hence, a proof of that the validator does what it's supposed to is not a proof that an axiom system is consistent.
Mod PDAllen's post up.
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.
> beautiful maths that have been discovered by mathematicians trying to solve it.
Indeed. I'd just started my math degree when Wiles's proof came out, and a prof of mine remarked---only half joking---that having the theorem proved was a terrible blow to mathematics.
The true value of FLT was its power to motivate and tantalize, spurring people to try all manner of wacky and creative ideas to find the simple proof that surely must exist...and enriching the rest of math with that creativity.
Had a computer proved FLT, the problem would have contributed vastly less to our knowledge.
"Mathematics is developed over decades and centuries. With a few notable exceptions, it doesn't just fall out of the sky in textbook form. Most areas of math started out as a giagantic mess (ex; calculus, linear algebra, even geometry), and it has taken the work of countless researchers, authors, and teachers to distill and refine it."
Well there goes the future of all those "new business models", and "the internet will save us".
It is quite a large step to go from raw computing power to intteligence. Sure computers will eventually have way more processing power than we humans do..hell they do right now if you assign them to a certain task, but that is a far cry from being intellent.
Neurosimulation researchers are emulating whole datapaths in the brain now. These datapaths have shown to be intelligent.
http://www.bhargav.com/books/Math/Fermats_Last_The orem_WILES.pdf
I think that the best explanation that I've seen regarding Fermat's famous comment about the margin being too small was that he did indeed think that he had proved it and later realized that he hadn't. The reason for thinking that this is true is that Fermat had a tendency to taunt his mathematical peers with theorems that he challenged them to prove. If he had solved the Last Theorem then undoubtedly he would have taunted some poor mathematician into trying to solve it!
"sweet dreams are made of this..."
This is absolutely true. One of the interesting ironies of mathematics is that mathematicians generally aren't interested in examining the foundations of math. Most mathematicians are content with a combination of intuition and definition to make sense of the nature of mathematical objects (points and lines in Euclidean geometry e.g., or natural/rational/irrational numbers). It takes a fairly compelling reason to convince mathematicians to sweat the foundational stuff, as the validity of non-Euclidean geometries needed the justification of new physics to really gain validity. But in general it's mainly the philosophers of math who bother themselves with questioning the nature/validity of things like number or proof.
As far as that might relate to this story, mathematicians have certainly done a more than satisfactory job demonstrating the efficacy of computation to solve any given computable problem. (That's why they call them computable, I guess.) The only question is whether the computers have been programmed satisfactorily to perform the computational component of the proof.
It's hard.
my point was supposed to be: what's an article about math doing in the Economist. It would be the equally odd if the article about maths appeared in Mother Jones.
It just seems out of place, that's all. Sort of like if Nature published a bit about Yukos. They're not really experts in the field.
But mostly, it was a cheap shot at the Economist.
Comment removed based on user account deletion
The most important thing about a proof is not that it shows that a proposition is valid in a system, but that it sheds light on the proposition to begin with.
I remember proving that 1+1=2 using Peano arithmetic in a Prolog based theorem prover called Ergo. It took me longer than you'd expect (and I was one of the very few who were able to prove that x+y = y+x for x,y in the natural numbers) and it would've been impossible without doing it, at least in part, by hand first. Everyone knows that 1+1 equals 2, but the trick is that few people know why. And a printout simply stating 'TRUE' does nothing to illuminate this.
You're pretty stubborn, isn't it? The theorem is true as far as any theorem is known to be true. Many mathematicians have tried to find flaws in the proof, nobody has managed to conjure up a counter-example so far. Just accept it: planar graphs are four-colourable, and any contiguous map is a planar graph.