Mizar Mathematical Library


The Mizar Mathematical Library (MML) consists of Mizar Articles. Two articles form the foundation of the library: All other texts undergo verification by Mizar to be correct consequences of those axioms. The Mizar system assists the author of a new text in preparing available terminology and results, verifies the claims of the text and extracts facts and definitions for inclusion into the library. The task of building a rich mathematical library is currently the main effort of the Mizar community. As of now the library includes 752 articles contributed by 137 authors, with about 20 of them active on a long term basis. Most of the library texts formalizes the fundamentals of introductory mathematics. Some of the texts contribute more advanced results.

Home | Project | Language | System | Library | JFM

Last modified: January 21, 2003