Kenneth Appel, of Appel-Haken Four Color Theorem Fame, died recently. See here for an obit.
In 1972 I read that the four-color theorem was an open problem. From what I read it seemed like there was some progress on it (e.g., results like `if its false the graph has to be yah-big) but it seemed to be years away from being solved. I assumed that a new idea was needed to solve it.
Then, in 1976, it was SOLVED by Appel-Haken. From what I read it wasn't so much a new idea but very clever use of old ideas and a computer program. I also heard that it was just at the brink of what computers could do at the time, and that it would have taken 1200 grad student hours. (There is a good description of the proof on Wikipedia here.)
At the time I heard there were objections to the proof. Later when I read some of them they didn't seem like real objections. They boiled down to either
- I wish there was a shorter proof. This is true, but not a reason to object.
- It can't be hand checked. I trust a computer-checker MORE THAN a human checker
- We don't know WHY its true. This is a more reasonable objection- but we do know how they got it down to a finite number of cases, so I'm happy with that.
In 1996 Robertson, Sanders, Seymour, Thomas was obtained a simpler proof. In 2005 Werner and Gontheir formalized the proof inside Coq- a proof assistant. To quote Wikipedia This removed the need to trust the various computer programs used to verify particular cases;it is only necessary to trust the Coq Kernel At this point I doubt anyone seriously doubts that the theorem has been proven.
There have been more computer-assisted proofs since then. See here for a list of some of them. That article also claims that such proofs are controversial and not always accepted. Is this really true? I thought the controversy was gone except for the topic of the next paragraph.
A famous computer assisted proof (or perhaps ``proof'') is the Kepler Conjecture. In 1998 Thomas Hale claims to have proven it. The proof involved rather complex computer calculations. The referees say they are 99% sure its true. Here's hoping an easier proof is found.
Computer assisted proofs may become more common. I just hope we still know WHY things are true.
Was Appel-Haken the first use of computer assisted proofs? I doubt it, but it was likely the first one to have an impact. It was important to know that this kind of proof could be done.
Is there a much shorter proof? A combinatorist once told me that since the function
f(n) = max size of proofs of statements of length n
grows faster than any computable functions, there have to be some statements that have very long proofs; and perhaps the four color theorem is one of them.
Thomas Hale is working with a team on a fully formalized proof of Kepler Conj., in the proof assistant HOL Light:
ReplyDeletehttp://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet
As I (sketchily) understand it, there is no hope or intention of getting a 'simple' proof in the usual sense; in fact there is going to be significantly more case analysis and numerical work than in the original proof, because computation is cheap and this will make the proof's superstructure more manageable.
I believe that one day formal proofs in Coq/Isabella will be the norm and not the exceptions. You will see conference committee saying: Proofs should be 10 pages of human readable abstract + comments together with the Coq proof (with a limit of 10Gb). It will play the role that latex will play in todays submission.
ReplyDelete"there have to be some statements that have very log proofs" -- so f(n) = O(log(n))! Neat! :)
ReplyDeleteCute!
DeleteI fixed the typo.
Actually VERY LOG might mean log(log) or log^*.
bad idea for a blog post: what would VERY log mean? or VERY followed
by a function. VERY square. VERY polynomial.
I believe and hope that mechanized proofs will be common in math and computer science in the future. Proof assistants such as Isabell and Coq increase the trust in the results and can sometimes help to organize and develop the proof. (Like programming on paper vs. programming with a computer.)
ReplyDeleteAre proof assistants still controversial? Absolutely. Some friends of mine are mathematicians and they are very skeptical about proof assistants. Some are claiming that formalizing proofs with them is just a waste of time since you don't get any insights. Others are claiming that it is impossible to use these tools. Another colleague who is a logician does not trust Coq because he does not understand its meta theory.
All this reminds me of the arguments that people make against new programming languages. I think that the reasons why people make such arguments are similar: They are scared by new things that they don't understand immediately and that might change the way they work.
There was a year-long program this year at the IAS on something called homotopy type theory, which is an extension of the logic used in Coq and makes it possible to talk directly about homotopy theory and higher category theory. This makes computer-assisted proofs in these areas *much* more feasible. This spring, we did computer-assisted proofs of some basic theorems in homotopy theory, like calculating some homotopy groups of spheres. These proofs are less like Kepler or four-color, where the proof assistant is helping handle the massive number of cases, and more like the recent computer-assisted proof of the Feit-Thompson odd-order theorem, which is more traditional math that just happens to be done on a computer. In the homotopy theory specifically, it's definitely the case that we are getting new insights out of the perspective on homotopy theory provided by type theory, and the process of doing the proofs in a proof assistant.
Deletehi LF great post thx much for the tip on the NYT article. its great you take a sensible view on this subj but its easy to see how the mathematicians are upset about this subject. theres some really exciting stuff happening over in timothy gowers blog on this subject, really urge CS types to check it out, some major cross pollination opportunities going on.
ReplyDeletehave been tracking this subj for many,many yrs. planning on putting up a way cool post with zillions of great links on the subj. if some who read this drop by my blog, drop me a comment & Ill write it up sooner rather than later. [can track exactly who does this by the referrer stats, wink]
in the meantime my blog has several links on the home page on the subject.
this also fits into what is called "empirical/experimental math" which is seeing some slow increase in spread/acceptance.
4color proof-- one of the greats of the 20th century if you ask me!
thx again for the great post/topic! hope to read more on the subj in future!
As a student in the 1970's I was teached that proof - computer or man driven - will forever be striked by the 'Godel theorem' malediction.. In other words: I always lie.. is true !
ReplyDelete