In a recent post to the vdash mailing list by Herman Geuvers there is an information that the application by the team at Radboud University Nijmegen, NL with participation from six other universities for funding of development of formalized math wiki was turned down. That is rather unfortunate. I didn’t like some of the specifics of the plan, but I think software created by the project, if released under free license could be reused to create something better. I am not too surprised that they didn’t get the money. Getting it was about as likely as EU funding the development of Wikipedia before it existed (I can image what a typical EU official would think about the idea of “online encyclopedia that everybody can edit”).
I have read Lee Smolin’s book “The Trouble with Physics” recently. The book is mostly about history of development of concepts in physics and science in general and how string theory came to dominate theoretical physics in recent years. Smolin is very good at creating the illusion of understanding of the stuff he writes about in his readers. I know it must be an illusion, because the book does not contain a single math formula, but still, the illusion is very convincing. The last part is devoted to philosophy of science and the the critique of how funding and hiring in academia work. To summarize, the main problem Smolin points out is that the current system of funding science is susceptible to fads and is biased against ideas that are new, radical and controversial. It works well for development in the framework of existing paradigms, but puts a very high barrier for ideas that would cause paradigm shifts.
Formalized mathematics is certainly not new, but it is kind of radical and it is definitely controversial. Even if the person consulted by a grant giving body is not hostile to the idea of machine checking proofs (as happens among mathematicians), the questions she would ask are like: What are practical applications of this? Does it advance creating new mathematics? Is it useful for teaching general general public about math? These are the same question that someone could ask in the second half of XIX century trying to evaluate the beginning of development of modern foundations of mathematics. Honest answers then would be: We don’t know, maybe this will allow to better judge validity of existing proofs. General public? Probably not. As for new mathematics, maybe in the future… The answers to these question for formalized mathematics are similar. We don’t know what will be the consequences of having a faithful machine representation of some larger part of mathematical knowledge. I think it will eventually lead to a deep change in how mathematics is done, but that is only my belief. For now I am pretty sure that many people (not in the sense of “general public”, but maybe 5% of students of mathematics) given a chance to learn writing real proofs would simply enjoy doing that.