In chats with models like deepseek the LLM makes many wrong claims, for example it doesn't know that the inverse image of a closed set by a continuous function is a closed set. Maybe more advanced models can in special circumstances, guided by the work of humans and Lean, prove theorems. But just like in RL, the brute force approach of failing a million times may not be enough when the reward is far.

In math the reward is finding the decomposition that reduces the problem to simpler cases, and in many cases that reward is very far. Furthermore, the LLM may process the many cases fast, but the decomposition often comes from a human, and the model takes the credit for the proof.