Approaches to Proving Hard Theorems

Peter Principle Points

• ATP systems can be (refutation) complete, but ...
  • They require infinite resources
  • The search space is O(N ^2SearchDepth)
• Realistically, they have PPPs

Allah or the Mountain

• Prove harder theorems by improving ATP systems

• Prove harder theorems by making them easier
  • Small changes can make large differences