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. Most of the library texts formalize the fundamentals of introductory mathematics. Some of the texts contribute more advanced results.

[ Home | Project | Language | System | People | MML | FM | SUM ]

Last modified: October 28, 2014