<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>

CC BY-SA 4.0
2018-12-05T09:10:02.717Z
2018-12-05T09:10:02.717Z
Oliver Mason
<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>

<logic><automated-theorem-proving><automated-reasoning><general-problem-solver>
When will we have computer programs that can compose mathematical proofs?
Siddhartha
# 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.


---

