Why ATP for Mizar

• Reasoning in very large theories is an interesting AI field
  • Mathematicians have many theorems and proofs in their heads
  • Need methods for selecting axioms, generating lemmas, learning from previous proofs, defining useful concepts, ...
  • SRASS, MaLARea, Paulson & Meng, Petr Pudlak
  • Submit your system to the new batch mode of CASC
  • Submit your paper to a special issue of JSC

• Mizar verifier has a complicated implementation
• Use ATP for independent verification of the MML (in this work, the MPTP Challenge problems)
• Mizar does not produce low-level proof objects:
  Use ATP proof objects to communicate with other proof assistants in large projects like Flyspeck
• Lots of mathematical problems for testing and improving ATPs