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?

  • $\begingroup$ The first step is to define what a mathematical proof is. In the famous “Logic theorist” program a proof is similar to a plan which brings system from start state into the goal state. The start-state might be “4+x=1-y” and the goal state is “x+y=-3”. If the software has found the transformations steps inbetween the equation has been proven. $\endgroup$ – Manuel Rodriguez Dec 5 '18 at 9:59

Arguably we have had this since 1957, with the 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 problem), but fails in real life, as real life is too complex for it to cope.

There is a list of solvers (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.

| improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.