Research map / Large language models / Agents, code and math
Lean Workbook: A large-scale Lean problem set formalized from natural language math problems
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.
Builds Lean Workbook, a ~57K formal-informal Lean 4 problem set produced by an iterative active-learning autoformalization pipeline with compile checks, back-translation NLI filtering, and human correction.
Problem
Formal theorem proving with LLMs in Lean is limited by the scarcity of formalized contest-level math statements; manual formalization is expensive.
Approach
An iterative active-learning autoformalization loop: fine-tune a translation model, translate AoPS forum problems to Lean 4, filter by Lean compilation and LLM-based back-translation NLI, have experts fix failure patterns, and retrain each round.
Key results
- Final dataset has 57231 formal-informal pairs passing NLI; manual check gives 93.5% weighted accuracy over sampled tags.
- InternLM2-Math-Plus fine-tuned with Lean Workbook reaches 50.4% on MiniF2F-valid and 46.7% on MiniF2F-test versus 44.3% and 37.3% with Mathlib alone.
- Proof search with InternLM-Math-Plus solves 4898 Lean Workbook problems at Pass@1024 (8.6%).
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Add human-labeled data through iterative fine-tuning | Final-round Model · Active learning dataset | CPN: 136670 -> 205079 | Helped |
| Add human-labeled data through iterative fine-tuning | Final-round Model · Active learning dataset | NPN: 37122 -> 57231 | Helped |
| Fine-tune on Lean Workbook | Final-round Model · Active learning dataset | CPN: 205079 -> 228928 | Helped |
| Fine-tune on Lean Workbook | Final-round Model · Active learning dataset | NPN: 57231 -> 82893 | Helped |
| Add Lean Workbook to training data | InternLM2-Math-Plus fine-tuned on Mathlib · MiniF2F-valid | accuracy: 44,3 -> 50.4 | Helped |
| Add Lean Workbook to training data | InternLM2-Math-Plus fine-tuned on Mathlib · MiniF2F-test | accuracy: 37.3 -> 46.7 | Helped |
| Use Lean Workbook Plus data for translation | Final-round Model · Number theory problems | translation correctness | Hurt |
Surprising findings
- Integer division ambiguity in Lean was only about half-correctly fixed even after adding human-labeled examples.
- Using an LLM (Qwen) for NLI-based back-translation filtering is imperfect; compile-passing translations often do not match the original question.
Limitations
- Near-duplicate problems in the dataset are hard to deduplicate.
- Focused on contest-level problems, may not suit other math levels.
- Errors in interpreting contest problems (e.g., integer vs real division, minimality) persist despite iteration.
Experimental setup
Datasets: MiniF2F ProofNet AoPS (Art of Problem Solving) forum problems Compfiles
Benchmarks: MiniF2F valid MiniF2F test Lean Workbook manual accuracy sampling IMO problems from Compfiles
Metrics: compile pass number NLI pass number correct translation rate accuracy Pass@1024
Baselines: Mathlib-only fine-tuning DeepSeek-Prover
Builds on: MiniF2F ProofNet Lean 4 Mathlib
Closest papers by meaning
- Herald: A Natural Language Annotated Lean 4 Dataset (ICLR 2025 · similarity 0.92)
- MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving (ICML 2025 · similarity 0.89)
- Lean-STaR: Learning to Interleave Thinking and Proving (ICLR 2025 · similarity 0.89)
- LeanAgent: Lifelong Learning for Formal Theorem Proving (ICLR 2025 · similarity 0.88)
- MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data (ICLR 2024 · similarity 0.88)
- miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward (NeurIPS 2025 · similarity 0.87)
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.