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