Why is there no AlphaZero for theorem proving?

It seems an obvious thing to try; therefore, it has been tried.

Impressive results are publicized; therefore it wasn't impressive.

There are. AlphaProof (Google) and DeepSeek-Prover already Monte Carlo Tree Search (MCTS) and use AlphaZero’s core reinforcement learning algorithms to prove theorems inside formal verification environments like Lean.

The problem is that Mathematics has countably infinite branching factor, game like Go has only max 361 possible moves at any point.

The problem is there's no "ever better opponent" to play against---in Go it was a slightly different version of the model itself---and creating one, e.g. creating an ever improving model that generates ever more difficult theorems to prove, hasn't AFAIK occurred yet.

You can make fake IMO test, perhaps a longer version that has 60 problems to get a better statistical result.

Lean or it didn't happen.

Reply on news.ycombinator.com