Fundamental Mathematical Theories

The Mathematical Theories

• Van-Neuman-Bernays-Gödel set theory [Qua92]
• Peano arithmetic
• Tarski's geometry
• Number theory [Qua92]

The ATP

• Encoded in first-order logic
• Challenge problems solved
  • Composition of homomorphisms is a homomorphism [Qua92]
  • Unique factorization theorem
  • Euler's generalization of Fermat's theorem
  • Löb's theorem
• Proofs using Otter

The Philosophy

• "Regular use of ATP ... state of bliss"
• "Maximize the integral of one's pleasure function over time"
• "The pot of gold: Immortality"
• "With the help of mathematicians ... we might live forever
• Art's invitation ... " join me in the loop"