The MPTP Challenge

• Two sets of 252 problems generated from a part of MML
• The 252 theorems recursively needed for one implication of the Bolzano-Weierstrass theorem (the root theorem of the Challenge)

• Hundreds of symbols and definitions, ca. 1400 TPTP formulas
• Symbols and formulas are named consistently in all problems
• A suitably large subDAG of the MML useful for experimenting with ATP methods in large theories
• The two sets differ in the amount of unnecessary axioms added to the problems ("all previous knowledge" vs. "only necessary knowledge")

• May 2007: only 199 of the 252 problems (79%) have been solved by any ATP system