What is Mizar?

• Project aimed at formalization of math
• Started in 1973 by Andrzej Trybulec
• Formal language for math (formulas, proofs)
  • Close to natural language
  • Understandable/verifiable by computer
• Verifier for articles written in the formal language
• Many other tools for refactoring and maintanance

• Mizar Mathematical Library (MML)
  • Large library (ca. 1000 articles) of formal articles based on set theory
  • New articles can use theorems and definitions from more basic articles (large DAG of theorems)
  • List of important theorems in Mizar: http://mmlquery.mizar.org