Theorem-prover training stops scaling data: 500 boundary-hard tasks mined from verified proofs lift both provers
Synopsis
Reinforcement learning for formal theorem proving is bottlenecked by scarce hard tasks: existing Lean problems are either already solved by current provers or too uninformative. ProofFrontier starts from verified Lean theorem–proof pairs, keeps each theorem statement unchanged, and hides proof-structural guidance around key local nodes so the prover must rediscover intermediate reasoning; base-prover pass rates then select tasks that are solvable in principle but not easily solved. GRPO training on 500 synthesized tasks improves DeepSeek-Prover-V2-7B and Goedel-Prover-V2-8B on miniF2F, ProofNet and PutnamBench over each base model.
Interpretation
The hard problems needed to train a formal theorem prover can be carved out of existing proofs rather than written as new theorem statements. Existing Lean corpora are either already solved by current provers, giving little learning pressure, or far beyond them, yielding mostly failed rollouts, so complete tasks that are both guaranteed solvable and hard are missing. On miniF2F, DeepSeek-Prover-V2-7B rises from 70.49 to 75.41 and Goedel-Prover-V2-8B from 77.87 to 81.15 after ProofFrontier training, both at a sample budget of 32, with results checked by Lean.
Each verified Lean proof is parsed into a local proof graph, structurally important nodes are scored, and a family of hints is generated at different visibility levels. The masked proof body is never an infilling target; masking only controls how much proof-structural information reaches the prover, and the theorem statement stays fixed. Nodes are scored by bridge, usage and change heuristics, visible fields are rendered into short hints, and difficulty is not assumed from the mask level but measured by base-prover pass rates under Lean verification.
Filtering keeps only tasks whose base-prover pass rate falls between more than 3 and fewer than 5 successes per 16 attempts. That band marks tasks no longer trivial yet still yielding informative verifier feedback, concentrating training near the prover's capability boundary. The main experiments train on 500 selected boundary-hard tasks; on miniF2F, 100 tasks raise the base score from 70.49 to 72.71, 250 reach 74.38, and 500 reach 75.41.
Perspective
The demonstrated scope is formal theorem proving in Lean, with training tasks built from verified theorem–proof pairs in the open-source Goedel-LM/SFT_dataset_v2 and evaluation on miniF2F, ProofNet and PutnamBench; the main experiments train on 500 selected tasks, and no ProofFrontier hints or reference proofs are provided at evaluation time.
Proof-structure masking rests on source-level heuristics, so structurally important nodes may not match the steps actually hard for a given prover; capability-aware filtering is model-dependent, and different base provers, decoding budgets or verifier settings may require recalibrating the hard-side selection; the auxiliary proof-similarity reward may bias the model toward the reference trajectory and under-reward alternative valid proofs.