MBase Related Efforts

History

The proposal for a general system-independent knowledge base for mathematics is not new: Around 1995, an anonymous group of authors put forward the QED Manifesto, which advocates building up a mathematical knowledge base (and supporting software systems) as a kind of "Human Genome Project" for the deduction community (QED activities). Unfortunately, the vision has failed to catch on in spite of a wave of initial interest. In my view this is due to the lack of supporting software, as well as well as to the ensuing debate on the "right" logical formalism.
In the MBASE project, we will try to do better and circumnavigate the problems of QED.

Repositories of Formal Mathematics

MBase is not alone: There are several large repositories of formalized mathematics, which we will list below. Our goal is to include these into MBase at some point giving the world a general interface to mathematical knowledge.

Mathematical Knowledge Management (MKM)

The MBase project is part of the larger MKM effort, which is interested in techniques for management of formal mathematical knowledge. The emerging research field has constituted itself at workshops at RISC Linz (September 2001) and McMaster University (June 2002). A third workshop is planned at Bertinoro (February 2003).

Informal Mathematics on the Web

There are various repositories of informal mathematics on the web, we list only a few of them here.

© 2006 Copyrights KWARC. | XHTML 1.0 | CSS | Page generated from XML sources with the WSML package