Research map / Large language models / Agents, code and math
LEGO-Prover: Neural Theorem Proving with Growing Libraries
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes LEGO-Prover, a neural theorem prover for Isabelle that builds proofs block-by-block from a growing, retrieval-based library of verified lemmas, which is expanded by an evolver using ChatGPT.
Problem
LLM-based theorem provers assume a fixed theorem library and generate whole proofs in one pass, so they fail on long-chain proofs and cannot reuse lemmas proved on other problems.
Approach
A prover decomposes problems into sub-goal lemmas retrieved from and added to a growing vector-store skill library of Isabelle-verified lemmas, while an evolver generalizes existing skills (four directional transformations) and solves requested sub-goals to keep enlarging the library.
Key results
- Achieves 57.0% pass rate on miniF2F-valid and 50.0% on miniF2F-test (cumulative with human and model informal proofs), beating Subgoal-Learning's 48.0% and 45.5%.
- Ablation with 50 attempts: removing the growing skill library drops valid pass rate from 50.4% to 47.1%.
- The generated skill library contains 22,532 verified skills.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use LEGO-Prover* instead of Subgoal-Learning | Theorem proving with ChatGPT · miniF2F-valid | success rate: 48.0% -> 57.0% | Helped |
| Use LEGO-Prover* instead of Subgoal-Learning | Theorem proving with ChatGPT · miniF2F-test | success rate: 45.5% -> 50.0% | Helped |
| Add the growing skill library, including the evolver (ablation) | LEGO-Prover · miniF2F-valid | success rate: 47.1% -> 50.4% | Helped |
| Use human-written instead of model-generated informal proofs | LEGO-Prover · miniF2F-valid | success rate: 52.4% -> 55.3% | Helped |
| Use human-written instead of model-generated informal proofs | LEGO-Prover · miniF2F-test | success rate: 45.5% -> 50.0% | Helped |
Surprising findings
- Plain-prover baselines like Thor (search with a fine-tuned 700M model) trail LLM-based methods by roughly 4.7% or more, and the authors attribute this to short policy steps enlarging the search space.
- Only about 24% of valid-set problems that passed verification used retrieved skills, and many solved problems did not need any skill, so direct reuse contributed fewer solves than expected.
Limitations
- Relies on expensive closed-source ChatGPT/GPT-4 API calls, making experiments costly.
- Many lemmas are trivial or already present in Isabelle's library, and direct reuse of skills contributed relatively few solved problems.
- Ablation only run with 50 attempts on the valid set, not the test set.
Experimental setup
Datasets: miniF2F MATH
Benchmarks: miniF2F-valid miniF2F-test
Metrics: pass rate
Baselines: Thor Thor + expert iteration Draft, sketch, and Prove Subgoal-Learning LEGO-Prover without skill library
Builds on: Draft, sketch, and prove Subgoal-Learning Voyager Thor
Closest papers by meaning
- ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis (ICML 2025 · similarity 0.91)
- miniCTX: Neural Theorem Proving with (Long-)Contexts (ICLR 2025 · similarity 0.91)
- PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition (NeurIPS 2024 · similarity 0.90)
- Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models (NeurIPS 2025 · similarity 0.89)
- STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving (ICML 2025 · similarity 0.89)
- Alchemy: Amplifying Theorem-Proving Capability Through Symbolic Mutation (ICLR 2025 · similarity 0.89)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.