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.

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.