Contents

The TPTP Mathematics Domains

• 8 subfields (15 algebra subsubfields)
• 78 axiomatisations
  • 122 axiom files (plus 930 Mizar axiom files)
• 6939 abstract problems
  • 11049 problem versions
• I'm a logician who trusts mathematicians

Mathematics in the TPTP Idiom

• Cross-verification of Mizar
• Development of Fundamental Mathematical Theories
• John Slaney's Quasigroups
• Results from the AIM project
• Formalisation with Sledgehammer in Isabelle
• Solution of the Robbins Problem

Mathematics in the LLM Idiom

• LLMs and the Robbins problem
• Logic (the TPTP) Saves the Day!