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.

• The QED project
• The libraries of the theorem provers Isabelle, PVS, IMPS, NuPrl, ILF, Coq,...
• The Mizar Mathematical Library is a large collection of formalized mathematics, that has been verified by the Mizar system. It even has its own journal, the Journal of Formalized Mathematics.
• The Digital Library of Mathematical Functions is a project at the National Institute of Standards that aims at creating a web-accessible successor to Abramowitz and Stegun's, Handbook of Mathematical Functions. We are currently trying to convert this to a form that is amenable to MBase inclusion, when it is released.
• The NuPrl group has a project called digital libraries project, which aims at building interactive digital libraries of formal algorithmic knowledge.It will be based mainly on the NuPrl mathematical library.
• The Maya is a system that manages the Development Graph. It shares some code with MBase and will be connected to it as a distribute MBase component as soon as possible.
• Projects as MoWGLI project and HELM aim at technologies for sophisticated and interoperable exploitation and representation of mathematical knowledge within the World Wide Web. Systems like MBase are potential parts or extensions of such technologies.

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.

• The Free Software Foundation has announced "GNUPedia - The free universal encyclopedia and learning resource", MBase is in sync with this and could one day form a node in this effort.
• MathWorld aka (Eric Weisstein's Treasure Troves)
• The MATHS project of Dick Botting
• MathSciNet, a searchable data base of the mathematical Reviews of the American Mathematical Society