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.