Freek Wiedijk has posted the slides from his talk “How to build a library of formalized mathematics” on the MathWiki Workshop in University of Edinburgh that took place in October. The slides present Freek’s view on the main reasons why there is no large scale effort to create a good and comprehensive library of formal mathematics. What I find striking is no mention of Metamath among “interesting” or even “not in the top five” category. I understand that one can not mention every project (although, are there that many that have been active for more than ten years?), but Metamath is the only formalized mathematics project that managed to build community and attract contributors working without any expectation of reward. There are other formalized mathematics projects that people contribute to, but the contributions are either work of graduate students getting their degrees this way or faculty doing research for which they get their salaries. Freek mentions Linux and Wikipedia as succesfull projects based on “benevolent dictatorship”, but not the only formalized mathematics project in this category.
Unfortunately the slides are rather sketchy and only illustrate the main points, so it is hard to guess what was actually said. I would be happy to find out what was discussed under “formalization for communication of mathematics” and “looks do matter”. I think the most important feature needed for attracting contributors is the ability to produce readable presentations that attract readers.
Formalized Mathematics 
April 23, 2008 at 12:03 pm |
“I think the most important feature needed for attracting contributors is the ability to produce readable presentations that attract readers.”
This is one important point.
Because whatever other way you might use it for you can think of (sharing lessons, finding better answer) readability is used everywhere. An author is also a reader even when he contributes….
I guess also the main obstacle is a system that allows incoherent states, within different realm.
The quest for a single large library wont be won and should not be fought.
A few big libraries will eventually emerge from a substrate of incoherence and partial attempts, but I doubt they will never be built upfront.
April 24, 2008 at 2:01 am |
“the main obstacle is a system that allows incoherent states, within different realm.”
I don’t quite see why this is difficult. All that is needed is to attach a set of revisions of the repository to each theorem such that the theorem is valid in the revisions from that set. This set would be always not-empty as a theorem is accepted to the repository only if it checks out with the current version when the author attempts to add it. I think in practice it would almost always contain the current version of the repository. The only way this may not be true is that someone modifies the statement of one of the theorems that the given theorem depends on. From my experience with formalized mathematics this almost never happens. If you need a different statement, you just add one more theorem.