mlsanityData to 14 Oct 2026

Lean Workbook: A large-scale Lean problem set formalized from natural language math problems

arXiv 2406.03847 ↗First posted 6 Jun 2024cs.CLcited by 122

Not on the map. Why?

Cited by 40 in LLM reasoning, but placed by its own abstract, which didn’t fit.

Abstract (arXiv)

Large language models have demonstrated impressive capabilities across various natural language processing tasks, especially in solving mathematical problems. However, large language models are not good at math theorem proving using formal languages like Lean. A significant challenge in this area is the scarcity of training data available in these formal languages. To address this issue, we propose a novel pipeline that iteratively generates and filters synthetic data to translate natural language mathematical problems into Lean 4 statements, and vice versa. Our results indicate that the synthetic data pipeline can provide useful training data and improve the performance of LLMs in translating and understanding complex mathematical problems and proofs. Our final dataset contains about 57K formal-informal question pairs along with searched proof from the math contest forum and 21 new IMO questions. We open-source our code at https://github.com/InternLM/InternLM-Math and our data at https://huggingface.co/datasets/InternLM/Lean-Workbook.

Key facts. Cited by 122 papers in the map (data through 14 Oct 2026). Builds on 24 of its 34 references that are in the map. First posted on arXiv 6 Jun 2024.

Builds on

24 of 34 references.

References · 24

  1. 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,459
  2. 2021Training Verifiers to Solve Math Word Problemscited by 10,109
  3. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,371
  4. 2023Qwen Technical Reportcited by 3,344
  5. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,392
  6. 2022Galactica: A Large Language Model for Sciencecited by 744
  7. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  8. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  9. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
  10. 2022Autoformalization with Large Language Modelscited by 263
  11. 2017Thinking Fast and Slow with Deep Learning and Tree Searchcited by 252
  12. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 234
12 more
  1. 2022HyperTree Proof Search for Neural Theorem Provingcited by 197
  2. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 192
  3. 2022Formal Mathematics Statement Curriculum Learningcited by 142
  4. 2019The Lean mathematical librarycited by 134
  5. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 132
  6. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 109
  7. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 98
  8. 2023FIMO: A Challenge Formal Dataset for Automated Theorem Provingcited by 55
  9. 2024MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Datacited by 43
  10. 2023Multilingual Mathematical Autoformalizationcited by 39
  11. 2023LLMSTEP: LLM proofstep suggestions in Leancited by 32
  12. 2024Autoformalizing Euclidean Geometrycited by 27

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2024: 11; 2025: 62; 2026: 49.

122 papers.

Sort:

By area:

  1. 2025MathArena: Evaluating LLMs on Uncontaminated Math Competitionscited by 297
  2. 2025The Landscape of Agentic Reinforcement Learning for LLMs: A Surveycited by 205
  3. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 197
  4. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 133
  5. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Provingcited by 101
  6. 2025CWM: An Open-Weights LLM for Research on Code Generation with World Modelscited by 93
  7. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 84
  8. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 81
  9. 2025Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpeningcited by 80
  10. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 79
  11. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Expertscited by 59
  12. 2024Herald: A Natural Language Annotated Lean 4 Datasetcited by 59
38 more
  1. 2025A Survey on Large Language Models for Mathematical Reasoningcited by 52
  2. 2025Solver-Informed RL: Grounding Large Language Models for Authentic Optimization Modelingcited by 45
  3. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experiencecited by 44
  4. 2024InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Searchcited by 34
  5. 2024HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Provingcited by 33
  6. 2024Reliable Evaluation and Benchmarks for Statement Autoformalizationcited by 32
  7. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 31
  8. 2025Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physicscited by 31
  9. 2025Chain-of-Reasoning: Towards Unified Mathematical Reasoning in Large Language Models via a Multi-Paradigm Perspectivecited by 29
  10. 2025Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Proverscited by 28
  11. 2025Leanabell-Prover: Posttraining Scaling in Formal Reasoningcited by 27
  12. 2025MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Provingcited by 24
  13. 2025ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Datacited by 23
  14. 2025RL Grokking Recipe: How Does RL Unlock and Transfer New Algorithms in LLMs?cited by 23
  15. 2025Solving Inequality Proofs with Large Language Modelscited by 21
  16. 2025Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graphcited by 21
  17. 2025ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimizationcited by 20
  18. 2025REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoningcited by 18
  19. 2025Mathesis: Towards Formal Theorem Proving from Natural Languagescited by 18
  20. 2025LeanExplore: A search engine for Lean 4 declarationscited by 18
  21. 2025Reliable Fine-Grained Evaluation of Natural Language Math Proofscited by 18
  22. 2025ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddingscited by 18
  23. 2025Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoningcited by 17
  24. 2025Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verificationcited by 17
  25. 2025Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Modelscited by 17
  26. 2025CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalizationcited by 16
  27. 2025StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusioncited by 16
  28. 2026M2F: Automated Formalization of Mathematical Literature at Scalecited by 15
  29. 2025MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?cited by 13
  30. 2025StepFun-Prover Preview: Let's Think and Verify Step by Stepcited by 13
  31. 2025Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalizationcited by 12
  32. 2026LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalizationcited by 12
  33. 2024Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learningcited by 11
  34. 2025MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curationcited by 10
  35. 2025ASSESS: A Semantic and Structural Evaluation Framework for Statement Similaritycited by 10
  36. 2026LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematicscited by 10
  37. 2026Formalizing Mathematics at Scalecited by 10
  38. 2026Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalizationcited by 10

50 most cited of 122 All 122 (JSON)