# Why is automated theorem proving so hard?

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?

• What makes you think that automated theorem proving is very similar to board games? Games have fixed set of rules and clear rewards, I can't see how that is the point for theorem proving? – Tim Oct 5 '20 at 16:23
• @Tim ATP: you are given a set of axioms, a set of inference rules and a goal statement. The process of proving the goal can be represented as tree traversal, where nodes are sets of already proven statements and edges - applications of inferences rules. The main problem is to recognize the most promising edges. Board games: you are given an initial state, a rule set (= a set of possible moves) and a set of winning states. The process of playing is represented as game tree traversal. The main problem is to decide which move to choose in a particular game state. Looks similar, doesn't it? – Ivan Ivanov Oct 5 '20 at 16:32
• I am not familiar with the state-of-the-art of ATP, but, to support your assumptions/conclusions, this post would benefit from having a link to a research paper or book that mentions or describes the state-of-the-art in this domain. Btw, welcome to AI SE :) – nbro Oct 5 '20 at 20:54

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.

• The first part of this answer is interesting, but the second part would really benefit from some facts: i.e. what is the state-of-the-art in automated theorem proving (maybe some cite some research paper that surveys the SOTA tools and results in this field)? – nbro Oct 7 '20 at 21:05
• @nbro Are you looking for facts about the psychology part or about decision theories for subsystems of mathematics? – Mitch Oct 7 '20 at 22:11
• Facts about the state-of-the-art in automated theorem proving. For example, you could say something like "with current systems, we were able to prove this conjecture $X$" (or something like that), and then you cite a research paper (or something reliable) that supports that claim. It may also be a good idea, if you find something, to link us to a research paper/book that describes more in detail what are the approaches and why they are not good. – nbro Oct 7 '20 at 22:21
• @nbro Sure... I can only hint at such things (like I've already done). But yes I'll attempt to clarify. (sadly the OP probably won't know to follow up here on AI but it is still a really good AI question. Hopefully others will chime in. – Mitch Oct 7 '20 at 23:46