HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (2019)

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.