The Mizar Mathematical Library

About the MML

• A large library of formally verified mathematics
• Published in the Journal of Formalized Mathematics
• Based on first-order classical logic and Tarski-Grothendieck set theory
• New theorems are build on previous theorems

Inside the MML

• Contains
  • Articles (over 1000), which contain
  • Theorems (over 45000), which contain
  • Natural deduction steps, which contain
  • Simple justifications
• The Mizar tool is a proof checker for MML theorerms