4 ms·
The QED project was started in 1993 to build a database of all mathematical knowledge. It died out because formalized mathematics does not yet resemble traditio
by jhuni 14y ago
The QED project was started in 1993 to build a database of all mathematical knowledge. It died out because formalized mathematics does not yet resemble traditional mathematics. All existing theorem provers and proof assistants such as Mizar, HOL, and Cow have major shortcomings. Very few people are working to improve formalized mathematics because there isn't any compelling profitable application of fully formalized mathematics.
http://www.cs.ru.nl/~freek/qed/qed.html http://www.cs.ru.nl/~freek/qed/qed.html
- nnq 14y ago...so it's one of those "someone has to do it to prove it can be done" or "someone has to first make it work to prove it's useful" problems? Hopefully there are a few madmen to start working at it and they will be wise enough to do it all "in the open": open source code and publication of all developments, "blog stye", instead of the "talking about only after you've really understood it" approach. I would throw a helping hand on the programming side and maybe devops, even throw a few bucks at it if one were to crowd-source and crowd-fund such an effort ...just because I find it "so cool". And I'm sure there are others that would help any group of "brilliant madmen" trying to do this, even without any imaginable profitable applications. But for now, I'm trying to wrap my head around what the QED project was trying to do and what it did... thanks for the directions to them!