Adding an extra point, one thing that makes this difficult is that a lot of this kind of research is not about applying existing ideas but coming up with something that has never been done before, and neutral networks are a lot worse with creativity than with pattern matching. It's also hard to get enough training examples, especially since you'd either want these to be in strict logical language or train a system to recognize whether a hundred page proof in natural language is rigorous or not. So it's like a very long maze where noody knows if you're getting closer to the exit or not, and in most rooms you have to come up with something original or discover a new dimension. And there's the aspect whereby a lot of significant research is: create a new abstraction, realize and convince others that this abstraction is useful and gives you new intuition that lets you solve new problems.