I'd be delighted to see "deep learning" produce a non-trivial breakthrough, but it feels like theorem proving must be about as hard as it gets for just learning a heuristic from piles of examples.
In particular, it's very easy to prove boring theorems, very hard to prove outstanding conjectures, and downright impossible to work out which theorems will turn out to be interesting.
I would like a thing where I put in a proposition and attempts are made at autocomplete style proofs of the proposition. Maybe you can do that with program synthesis techniques and Lean style theorem provers.
I'd be delighted to see "deep learning" produce a non-trivial breakthrough, but it feels like theorem proving must be about as hard as it gets for just learning a heuristic from piles of examples.
In particular, it's very easy to prove boring theorems, very hard to prove outstanding conjectures, and downright impossible to work out which theorems will turn out to be interesting.