The search space for proofs is far bigger and less structured than a Go game. A lot of proofs also require creativity, in the sense that they aren't just "find the set of logical steps from 'initial condition' to 'proof'", but they require auxiliary theorems, definitions and constructions that help make the problem manageable.

Another problem is that a lot of proofs starts by exploration. For example, certain bounds for functions or convergence rates are proved without knowing what will be the end result.

Of all the problems that ML could be applied to, I find mathematical proofs one of the least promising. One, I don't see enough similarity between proofs that would allow any algorithm to learn useful patterns; and two, I don't think most mathematicians would trust a proof that cannot be understood (even if the output is a set of steps for a formal system, I imagine translating that to human language could be quite difficult).