Conclusion

The TPTP World loves Maths

• The mathematical notion determines ...
  • The representation requirements, which determine ...
    • The syntax of the representation, which determine ...
      • The ATP requirements, which determine ...
        • The choice of ATP system

Maths loves the TPTP World

• Encoding mathematics in TPTP problems ...
  • Enforces precise formalisation, which ...
    • Reveals weaknesses in informal (human) presentations, and ...
      • Permits proofs to be formally verified, even ...
        • Beyond human capability