Answers.Body: <p>Arguably we have had this since 1957, with the <a href="https://en.wikipedia.org/wiki/General_Problem_Solver" rel="nofollow noreferrer">General Problem Solver</a>. However, it is a thorny problem, and like so much in AI, it works fine in toy domains (like the <a href="https://en.wikipedia.org/wiki/Tower_of_Hanoi" rel="nofollow noreferrer">Towers of Hanoi</a> problem), but fails in real life, as real life is too complex for it to cope.</p>
  
  <p>There is <a href="https://en.wikipedia.org/wiki/Solver" rel="nofollow noreferrer">a list of solvers</a> (the category of programs dealing with this issue) on Wikipedia. As of today, it comprises about 40 systems (split into two sub-categories). These work with mathematical equations and presumably also more general problems, assuming they are not too complex.</p>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2018-12-05T09:10:02.717Z
Answers.LastActivityDate: 2018-12-05T09:10:02.717Z
Answers.UserDisplayName: Oliver Mason
Body: <p>When will it be possible to give a computer program a bunch of assumptions and ask it if a certain statement is true or false, giving a proof or a counterexample respectively?</p>
  
Tags: <logic><automated-theorem-proving><automated-reasoning><general-problem-solver>
Title: When will we have computer programs that can compose mathematical proofs?
UserDisplayName: Siddhartha
ThreadText: # When will we have computer programs that can compose mathematical proofs?
  
  (Asked by: username_0 on 2018-12-05)
  
  When will it be possible to give a computer program a bunch of assumptions and ask it if a certain statement is true or false, giving a proof or a counterexample respectively?
  
  **Tags:** logic, automated-theorem-proving, automated-reasoning, general-problem-solver
  
  ---
  
  ## 1 answers
  
  ### Answer by username_1 on 2018-12-05. Score: 2
  
  Arguably we have had this since 1957, with the [General Problem Solver](https://en.wikipedia.org/wiki/General_Problem_Solver). However, it is a thorny problem, and like so much in AI, it works fine in toy domains (like the [Towers of Hanoi](https://en.wikipedia.org/wiki/Tower_of_Hanoi) problem), but fails in real life, as real life is too complex for it to cope.
  
  There is [a list of solvers](https://en.wikipedia.org/wiki/Solver) (the category of programs dealing with this issue) on Wikipedia. As of today, it comprises about 40 systems (split into two sub-categories). These work with mathematical equations and presumably also more general problems, assuming they are not too complex.
  
  
  ---
  
  