But ML could in theory accelerate the process. For example, AlphaZero uses ML to highlight the correct paths in search algorithms. The same search algorithms exist for stockfish and both can reach the same conclusions, but, AlphaZero ends up looking up much shorter distance than stockfish, yet it wins. If anything, it is significantly more human-like than stockfish.

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).

I would like to bring up Gödel and his idea that you could construct theorems by multiplying equivalent numbers that represent theorems but I am sure you are well aware of it.

My argument is that it all happens through the application of operators and abstractions i.e. other numbers going through Gödel's approach.

In the same vein, we "should" in theory produce something similar. In RL, we have agents that learn to 'imagine' goals and then achieve them. Given the correct representation of such 'dreams' the models 'could' in theory learn to achieve such auxiliary theorems.

I wish we'd start with general loop variant/invariant generation...

Proof checkers are an existing technology. That's what CoQ is.

Yes. My formulation was sloppy - I didn't mean "unless" to imply that there can't be a prover. My argument was that without a full prover, you won't have a useful fitness function at all.

And even then recall/precision need to be 100%. And even if you could achieve that, you still end up with something that... generates statements that are provably true. Mild yay.

But that's not the problem. We can generate plenty of those. You want to identify the ones that actually advance the state of knowledge usefully.