Why is automated theorem proving so hard?

Question

The problem of automated theorem proving (ATP) seems to be very similar to playing board games (e.g. chess, go, etc.): it can also be naturally stated as a problem of a decision tree traversal. However, there is a dramatic difference in progress on those 2 tasks: board games are successfully being solved by reinforcement learning techniques nowadays (see AlphaGo and AlphaZero), but ATP is still nowhere near to automatically proving even freshman-level theorems. What does make ATP so hard compared to board games playing?

Answer 1

There are two ways to look at the problem, one in terms of logic and the other in terms of psychology.

To get any -start- on automation of mathematics, you need to formalize the part you want. It has only been since the early part of the 20th c that most day to day math had been formalized with logic and set theory. And even though Gödel's incompleteness theorems say (very loosely) that there is no algorithm to decide theorem-hood for mathematical statements (that include a theory of arithmetic), that still leaves a lot of math that -can- be decided. But that has taken the Reverse Mathematics program (still ongoing) to say specifically what subsets of math are decidable or to what degree (what logical assumptions are necessary) they are undecidable.

So theorems in arithmetic of just '+' (that is, dropping '*') can be decided, Euclidean geometry can be decided, single variable differential calculus can be decided but not single variable integral calculus. These examples show that what we know to be decidable is pretty elementary. And most of the things we care about are very un-elementary (almost by definition).

As to psychology, the theorems and proofs that you learn in mathematics classes are nowhere near like their formalizations. Most mathematicians aren't pushing symbols around in their heads like a computer does. A mathematician is more like an artist, visualizing dreams and connecting metaphors just on their barely conscious images borne out of repetition. That is, machines and mathematicians just work on different representations (despite what non-mathematicians might imagine).

---

To address your specific question, yes, mathematical theorems and the systems to prove them are very similar in a technical sense. Games (often, not always) can be modeled as trees, And likewise proofs can often be modeled as trees. Without writing you a library of books about games and proofs, let's just say that the mathematical proofs that are like games that are won by Alpha Zero are not for particularly interesting theorems. Winning a game of go is more like proving that a very very large boolean formula. Most mathematical theorems require a lot of ingenuity in introducing steps in their proof trees. It may be mechanical after the fact to check that a proof is correct, but discovering the proof almost needs magic to come up with a step in the game. Sure, some things in math are automatable (as mentioned before, derivatives), but some mathematical systems (such as integration) are provably impossible to find proofs of all true statements.

Another difference between theorem proving and games is that proofs have to be air tight on all paths, whereas with games one side just has to eke out a single win over the other side.

---

A separate issue entirely that may contribute to the difficulty is that we just may not yet have the tooling available, ie editors, notation, proof assistants that make it easy to do what should be easy. Or it could just be that mathematicians don't have the fluency with theorem proving systems.

Or it could be that if there were automated theorem provers good enough, mathematicians just wouldn't care too much for them because they'd take away the fun of finding the proofs themselves.