When will we have computer programs that can compose mathematical proofs?
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.