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.