mlsanityData to 7 Oct 2026

Formal Mathematics Statement Curriculum Learning

arXiv 2202.01344 ↗First posted 3 Feb 2022cs.LG cs.AIcited by 141

Not on the map. Why?

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

Abstract (arXiv)

We explore the use of expert iteration in the context of language modeling applied to formal mathematics. We show that at same compute budget, expert iteration, by which we mean proof search interleaved with learning, dramatically outperforms proof search only. We also observe that when applied to a collection of formal statements of sufficiently varied difficulty, expert iteration is capable of finding and solving a curriculum of increasingly difficult problems, without the need for associated ground-truth proofs. Finally, by applying this expert iteration to a manually curated set of problem statements, we achieve state-of-the-art on the miniF2F benchmark, automatically solving multiple challenging problems drawn from high school olympiads.

Key facts. Cited by 141 papers in the map (data through 7 Oct 2026). Builds on 27 of its 46 references that are in the map. First posted on arXiv 3 Feb 2022.

Builds on

27 of 46 references.

References · 27

  1. 2018BERT: Pre-training of Deep Bidirectional Transformers for Language Understandingcited by 40,204
  2. 2021Learning Transferable Visual Models From Natural Language Supervisioncited by 33,456
  3. 2020Language Models are Few-Shot Learnerscited by 32,199
  4. 2019EfficientNet: Rethinking Model Scaling for Convolutional Neural Networkscited by 6,415
  5. 2020Scaling Laws for Neural Language Modelscited by 6,411
  6. 2018A Style-Based Generator Architecture for Generative Adversarial Networkscited by 5,986
  7. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,203
  8. 2021Zero-Shot Text-to-Image Generationcited by 4,276
  9. 2016Google's Neural Machine Translation System: Bridging the Gap between Human and Machine Translationcited by 1,471
  10. 2019Dota 2 with Large Scale Deep Reinforcement Learningcited by 1,084
  11. 2017Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithmcited by 723
  12. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
15 more
  1. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  2. 2018Learning a SAT Solver from Single-Bit Supervisioncited by 198
  3. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  4. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  5. 2016DeepMath - Deep Sequence Models for Premise Selectioncited by 80
  6. 2018GamePad: A Learning Environment for Theorem Provingcited by 48
  7. 2017Deep Network Guided Proof Searchcited by 47
  8. 2017Premise Selection for Theorem Proving by Deep Graph Embeddingcited by 44
  9. 2020INT: An Inequality Benchmark for Evaluating Generalization in Theorem Provingcited by 44
  10. 2016Holophrasm: a neural Automated Theorem Prover for higher-order logiccited by 29
  11. 2019Learning to Reason in Large Theories without Imitationcited by 27
  12. 2020First Neural Conjecturing Datasets and Experimentscited by 26
  13. 2021Subgoal Search For Complex Reasoning Taskscited by 21
  14. 2021Training a First-Order Theorem Prover from Synthetic Datacited by 8
  15. 2020IsarStep: a Benchmark for High-level Mathematical Reasoningcited by 7

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2022: 17; 2023: 20; 2024: 41; 2025: 38; 2026: 25.

141 papers.

Sort:

By area:

  1. 2023RT-2: Vision-Language-Action Models Transfer Web Knowledge to Robotic Controlcited by 2,993
  2. 2023A Survey of Large Language Modelscited by 2,537
  3. 2023PaLM-E: An Embodied Multimodal Language Modelcited by 2,037
  4. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,359
  5. 2022STaR: Bootstrapping Reasoning With Reasoningcited by 895
  6. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  7. 2023Llemma: An Open Language Model For Mathematicscited by 385
  8. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  9. 2024Monte Carlo Tree Search Boosts Reasoning via Iterative Preference Learningcited by 238
  10. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  11. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  12. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
38 more
  1. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 173
  2. 2022A Review on Language Models as Knowledge Basescited by 156
  3. 2023Progressive-Hint Prompting Improves Reasoning in Large Language Modelscited by 147
  4. 2022Signal Propagation in Transformers: Theoretical Perspectives and the Role of Rank Collapsecited by 136
  5. 2024From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Modelscited by 136
  6. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  7. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
  8. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
  9. 2022Unveiling Transformers with LEGO: a synthetic reasoning taskcited by 105
  10. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 97
  11. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Provingcited by 96
  12. 2025Multiagent Finetuning: Self Improvement with Diverse Reasoning Chainscited by 90
  13. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 82
  14. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  15. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 78
  16. 2025Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpeningcited by 78
  17. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 77
  18. 2022NaturalProver: Grounded Mathematical Proof Generation with Language Modelscited by 72
  19. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 64
  20. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  21. 2023FIMO: A Challenge Formal Dataset for Automated Theorem Provingcited by 54
  22. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 52
  23. 2023Magnushammer: A Transformer-Based Approach to Premise Selectioncited by 50
  24. 2025Aristotle: IMO-level Automated Theorem Provingcited by 47
  25. 2024Learning Formal Mathematics From Intrinsic Motivationcited by 45
  26. 2024MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Datacited by 43
  27. 2023Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Provingcited by 37
  28. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experiencecited by 36
  29. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
  30. 2024LeanAgent: Lifelong Learning for Formal Theorem Provingcited by 34
  31. 2024InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Searchcited by 34
  32. 2024AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinementcited by 33
  33. 2024How Far Are We From AGI: Are LLMs All We Need?cited by 31
  34. 2024Automated Proof Generation for Rust Code via Self-Evolutioncited by 31
  35. 2024LLMPhy: Parameter-Identifiable Physical Reasoning Combining Large Language Models and Physics Enginescited by 29
  36. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 28
  37. 2025Leanabell-Prover: Posttraining Scaling in Formal Reasoningcited by 27
  38. 2025Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physicscited by 27

50 most cited of 141 All 141 (JSON)