Reinforcement-learning-trained AI theorem provers silently waste compute by generating the same failed proof attempts over and over.
Researchers studying DeepSeek-Prover-V1.5-RL on the standard miniF2F benchmark found that doubling the number of proof attempts from 32 to 64 solved exactly zero additional theorems - 42 out of 244 either way. The culprit is mode collapse: the model converges on a narrow band of tactics and keeps replaying them. Swapping in a fixed schedule of 15 structural "tactic skeletons" broke the plateau, recovering a 45% relative improvement at half the sampling budget (k=16), with an average gain of 12.3 theorems across three independent runs. Crucially, simply paraphrasing prompts did nothing, and adding irrelevant Lean comments actively made things worse.
This matters because theorem proving is one of the clearest tests of whether AI can do rigorous formal reasoning - and scaling alone is failing it. The finding suggests that RL training creates proof capability but simultaneously narrows the model's output diversity, a dynamic that more GPU time cannot fix on its own.
The effect is RL-specific: a base model without RL training proved zero theorems regardless of intervention, and a model trained with supervised fine-tuning instead of RL showed no benefit either. A second RL-trained model, DeepSeek-Prover-V2-7B, hit three frontier proofs that no baseline configuration could reach - further evidence that structural diversity is doing real work, not just reshuffling existing wins. For anyone benchmarking these systems, the implicit assumption that more samples equals more coverage is worth revisiting.