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 that contain
  • Theorems that contain
  • Natural deduction steps that contain
  • Simple justifications
• The Mizar tool is a proof checker for MML theorems