Plus there isn't a lot of training data in lean.
Most gains come from training on stuff already out there, not really the RLVR part which just amps it up a bit.
Turing machines are also deterministic, but there is no algorithm that can decide whether any given Turing machine halts. What you're asking for is a solution to the Halting Problem.
That's the first problem, the second problem is that any such system that didn't support natural language would require a formal language of some sort, and then you would have to convince every mathematician to write their proofs in your language so it can be checked. All attempts at this have failed to gain much traction, although Lean has gotten pretty far.
It's like Chess, checking who wins for a given board state is easy, but coming up with the next move is hard.
Of course, one can try all possible moves and see what happens. Similar to Chess AI based on search methods (e.g. MinMax), there are proof search methods. See the related work section of the paper.