Cross-verification of the
Mizar Mathematical Library

The Mizar Mathematical Library

Cross-verification Approach

• Convert Mizar theorems to first-order problems
• Prove the first-order problems
• Convert Mizar proofs to first-order derivations
• View and verify the first-order derivations

Progress

• 40% of non-arithmetic first-order problems proved
• Projected 99% of simple justifications proved
• 51% of root theorems verified by GDV

Application of ATP

• Theorems and proofs converted to TPTP format
• ATP systems used to prove problems
• GDV used to verify derivations
• IDV used to view derivations

See the Mizar and TPTP forms online at tptp.org/MizarTPTP

---