Recent papers I know of are Deep Network Guided Proof Search and Deep Math. Both of these reduce the search-space of current non-ML based theorem-provers by suggesting the next premise or tactic to use, pruning the search tree. (Quite similar to how Alpha Zero still relies on traditional game-tree search, but heavily prunes it!)
A more direct approach taken by End to End Differentiable Proving focuses on the backward chaining proof search technique. It replaces the hard decision of which variable to substitute into which rule (for example: substitute "John" into the rule: If Human(x) then Alive(x)) with a scoring function which assigns a number to how good each possible substitution is. Then a beam-search is used to find the highest scoring set of substitutions.
I would contest the idea that finding proofs can't be solved using pattern recognition -- I rely on a lot on my intuition when proving things, which pretty much just guesses which direction to try next based on similar problems I've seen before. This approach seems quite similar to above papers. In other words, my intuition performs pattern recognition.
On the other hand, current theorem provers -- either with or without ML -- are quite weak compared to human provers, so I wouldn't try to prove the Jacobian conjecture with one.