Proving math theorems with computers is hard; they often must search through many possible steps. A new system, Reap, uses a tree-search method inside the Lean proof assistant to guide that search with a small neural network. The final model (Reaper-1) solves 79.9% of a standard math benchmark, matching much larger systems. It also reveals that training via helps the prover take more direct, effective steps rather than many small adjustments.
Training shifts a small theorem prover toward fewer, larger proof steps
A 1.7B-parameter prover trained with search-based reinforcement learning solves 79.9% of miniF2F-test, and its search logs show it moving from many small local edits to fewer, more elaborate tactic steps built around intermediate claims.
Top University
Yutong Wang · Xuanzhi Ren · Tianyi Xu · Ruitong Liu · Jingda Xu · Peihao Wu · +2 more
Peking University · IQuest Research · Beijing International Center for Mathematical Research · New Cornerstone Science Laboratory · Center for Machine Learning Research, Peking University
Research Digest··3 min read
In one line
Reap trains a 1.7B-parameter prover that solves 79.9% of miniF2F-test via Monte Carlo search.
Before you read this
Two ideas this paper builds onRead it as
The authors release Reap, an open framework that runs Monte Carlo tree search inside the Lean 4 proof assistant, and use it to train Reaper-1, a 1.7B-parameter model.
Reap implements policy-value-guided directly as a Lean 4 tactic, so proof-state transitions, AND-OR search, budget control, proof reconstruction and replay verification all run inside the proof assistant.
How it works
stage by stageThe Daily Edition
The front page in your inbox each weekday morning: the lead, the picks, and why each one earned its place.