I don't think so. I'm not really competent to say if the NLP part will be solved soon, but (fully) automated theorem proving is very hard, and I don't see deep

I don't think so. I'm not really competent to say if the NLP part will be solved soon, but (fully) automated theorem proving is very hard, and I don't see deep learning applying to it very well. What could happen, though (hopefully), is that mathematicians start using more and more the various proof assistants (Coq, Isabelle/HOL, lean, …). These allow to write definitions, statements, theorems in a more programming-like way, with structured proofs; to develop modular libraries; and even in some cases to use automated provers to wave away details of the proofs. The problem of adoption of such provers, however, is a culture problem, not really a technology problem: as said elsewhere, mathematicians do not seem to care too much about formal correctness. It's only if automated tools help gaining insights (automatic search for (counter)examples, for example; function plotting; builtin algebra solving system… ?) that they will convince more people to use them. Modularity might also be a selling point, but not sufficient to overcome the steep learning curve of these tools. I have some hopes in [lean](https://github.com/leanprover/lean https://github.com/leanprover/lean), a new proof assistant inspired from Coq, which puts the focus on good UI and automation.