Kepler's conjecture about the optimal packing of balls in 3D was finally proved by Thomas Hales in 1998. Or was it ? Since 1999, a 12-member review committee of the Annals of Mathematics has been going over the proof in order to verify it. The NYT reported nearly two years ago that there were problems in the verification process, and now we hear the details, on Thomas Hales' Flyspeck page:
Robert MacPherson, editor of the Annals, wrote a report that statesInterestingly, Gabor Fejes Tóth, the chief referee, wrote a report certifying that he was "99%" confident of the proof, but no more, and the editor therefore concluded that
``The news from the referees is bad, from my perspective. They have not been able to certify the correctness of the proof, and will not be able to certify it in the future, because they have run out of energy to devote to the problem. This is not what I had hoped for.''
it's not enough for complete certification as correct, for two reasons. First, rigor and certainty was what this particular problem was about in the first place. Second, there are not so many general principles and theoretical consistencies as there were, say, in the proof of Fermat, so as to make you convinced that even if there is a small error, it won't affect the basic structure of the proof.''Apparently, the Annals will publish a paper on this topic with a disclaimer stating that the computer parts of the proof have not been verified. In the meantime, (and here's the collaborative aspect of this), Thomas Hales and others have undertaken a joint effort to rewrite his proof in a computer-verifiable form using OCAML. The project is called Flyspeck, and the page contains information on how to "participate" in the proof:
The first step is to learn the relevant background material:
See the resources listed at the bottom of the page for more information about these topics.
- Objective CAML,
- HOL light, and
- the idea of the proof of the Kepler Conjecture.
The second step is to become an experienced user. In practical terms, this means being able to create your own proof in the HOL light system.
If you have successfully proved a non-trivial theorem in the HOL light system, then contact Thomas C. Hales (http://www.math.pitt.edu/~thales) if you wish to participate.
(HT: sigfpe)
As someone who has played with collaborative filtering, I would probably add that distinguishing "web" from "collaborative" is hard. In effect, the web is, almost by definition, a collaborative effort.
ReplyDeleteI know people talk about Web 2.0 as the "collaborative web", but back in 1999, the first non trivial web app. I wrote was a posting board. This was 1999. It was all about collaboration. And how did I apply it? I setup a wavelet posting board on ondelette.com. I repeat: this was 1999.
Yes, we have better tools now but I would claim that the web was always about getting people to share information and work better together.
Posted by Daniel Lemire