Answers.Body: <p>There are two ways to look at the problem, one in terms of logic and the other in terms of psychology.</p>
  <p>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 <a href="https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems" rel="nofollow noreferrer">Gödel's incompleteness theorems</a> 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 <a href="https://en.wikipedia.org/wiki/Reverse_mathematics" rel="nofollow noreferrer">Reverse Mathematics program</a> (still ongoing) to say specifically what subsets of math are decidable or to what degree (what logical assumptions are necessary) they are undecidable.</p>
  <p>So <a href="https://en.wikipedia.org/wiki/Presburger_arithmetic" rel="nofollow noreferrer">theorems in arithmetic of just '+'</a> (that is, dropping '*') can be decided, <a href="https://en.wikipedia.org/wiki/Euclidean_geometry#Axiomatic_formulations" rel="nofollow noreferrer">Euclidean geometry</a> <a href="https://en.wikipedia.org/wiki/Tarski%E2%80%93Seidenberg_theorem" rel="nofollow noreferrer">can be decided</a>, single variable differential calculus can be decided but <a href="https://en.wikipedia.org/wiki/Richardson%27s_theorem" rel="nofollow noreferrer">not single variable integral calculus</a>. 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).</p>
  <p>As to psychology, the theorems and proofs that you learn in mathematics classes are nowhere near <em>like</em> 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).</p>
  <hr />
  <p>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 <em>are</em> automatable (as mentioned before, derivatives), but some mathematical systems (such as integration) are provably impossible to find proofs of all true statements.</p>
  <p>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.</p>
  <hr />
  <p>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.</p>
  <p>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.</p>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2020-10-07T21:05:12.193Z
Answers.Text: 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)?
Answers.UserDisplayName: nbro
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2020-10-07T22:11:14.607Z
Answers.Text: @nbro Are you looking for facts about the psychology part or about decision theories for subsystems of mathematics?
Answers.UserDisplayName: Mitch
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2020-10-07T22:21:18.910Z
Answers.Text: 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.
Answers.UserDisplayName: nbro
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2020-10-07T23:46:59.420Z
Answers.Text: @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.
Answers.UserDisplayName: Mitch
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2022-12-10T00:48:33.523Z
Answers.Text: I'm curious if we get to the point where an AI can prove everything a human can prove including some uninteresting theorems beyond a humans reach but the AI is unable prove anything new/uninteresting. It's one thing to train something to be good enough at what we already know, I think its an even more difficult problem to design a system to synthesize BEYOND what we know/could do (though I don't doubt it will be possible one day)
Answers.UserDisplayName: Sidharth Ghoshal
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2020-10-05T18:29:53.880Z
Answers.LastActivityDate: 2020-10-08T03:13:13.410Z
Answers.LastEditDate: 2020-10-08T03:13:13.410Z
Answers.UserDisplayName: Mitch
Body: <p>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?</p>
  
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2020-10-05T16:23:19.537Z
Comments.Text: 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?
Comments.UserDisplayName: Tim
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2020-10-05T20:54:47.880Z
Comments.Text: 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 :)
Comments.UserDisplayName: nbro
Tags: <automated-theorem-proving><automated-reasoning>
Title: Why is automated theorem proving so hard?
UserDisplayName: Ivan Ivanov
ThreadText: # Why is automated theorem proving so hard?
  
  (Asked by: username_0 on 2020-10-05)
  
  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?
  
  **Tags:** automated-theorem-proving, automated-reasoning
  
  > **Comments:**
  > **username_1**: 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?  
  > **username_2**: 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 :)  
  
  ---
  
  ## 1 answers
  
  ### Answer by username_3 on 2020-10-05. Score: 4
  
  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](https://en.wikipedia.org/wiki/G%C3%B6del%27s_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](https://en.wikipedia.org/wiki/Reverse_mathematics) (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 '+'](https://en.wikipedia.org/wiki/Presburger_arithmetic) (that is, dropping '\*') can be decided, [Euclidean geometry](https://en.wikipedia.org/wiki/Euclidean_geometry#Axiomatic_formulations) [can be decided](https://en.wikipedia.org/wiki/Tarski%E2%80%93Seidenberg_theorem), single variable differential calculus can be decided but [not single variable integral calculus](https://en.wikipedia.org/wiki/Richardson%27s_theorem). 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.
  
  > **Comments:**
  > **username_2**: 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)?  
  > **username_3**: @username_2 Are you looking for facts about the psychology part or about decision theories for subsystems of mathematics?  
  > **username_2**: 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.  
  > **username_3**: @username_2 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.  
  > **username_4**: I'm curious if we get to the point where an AI can prove everything a human can prove including some uninteresting theorems beyond a humans reach but the AI is unable prove anything new/uninteresting. It's one thing to train something to be good enough at what we already know, I think its an even more difficult problem to design a system to synthesize BEYOND what we know/could do (though I don't doubt it will be possible one day)  
  
  ---
  
  