mlsanityData to 7 Oct 2026

MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics

arXiv 2109.00110 ↗First posted 31 Aug 2021cs.AI cs.FL cs.LGcited by 380

Not on the map. Why?

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

Abstract (arXiv)

We present miniF2F, a dataset of formal Olympiad-level mathematics problems statements intended to provide a unified cross-system benchmark for neural theorem proving. The miniF2F benchmark currently targets Metamath, Lean, Isabelle (partially) and HOL Light (partially) and consists of 488 problem statements drawn from the AIME, AMC, and the International Mathematical Olympiad (IMO), as well as material from high-school and undergraduate mathematics courses. We report baseline results using GPT-f, a neural theorem prover based on GPT-3 and provide an analysis of its performance. We intend for miniF2F to be a community-driven effort and hope that our benchmark will help spur advances in neural theorem proving.

Key facts. Cited by 380 papers in the map (data through 7 Oct 2026). Builds on 15 of its 25 references that are in the map. First posted on arXiv 31 Aug 2021.

Builds on

15 of 25 references.

References · 15

  1. 2020Language Models are Few-Shot Learnerscited by 32,199
  2. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,203
  3. 2018GLUE: A Multi-Task Benchmark and Analysis Platform for Natural Language Understandingcited by 4,854
  4. 2016SQuAD: 100,000+ Questions for Machine Comprehension of Textcited by 4,115
  5. 2016The LAMBADA dataset: Word prediction requiring a broad discourse contextcited by 960
  6. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  7. 2019Analysing Mathematical Reasoning Abilities of Neural Modelscited by 331
  8. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  9. 2019The Lean mathematical librarycited by 127
  10. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  11. 2021NaturalProofs: Mathematical Theorem Proving in Natural Languagecited by 80
  12. 2019Graph Representations for Higher-Order Logic and Theorem Provingcited by 55
3 more
  1. 2020INT: An Inequality Benchmark for Evaluating Generalization in Theorem Provingcited by 44
  2. 2016Holophrasm: a neural Automated Theorem Prover for higher-order logiccited by 29
  3. 2019Learning to Reason in Large Theories without Imitationcited by 27

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2022: 10; 2023: 20; 2024: 56; 2025: 141; 2026: 153.

380 papers.

Sort:

By area:

  1. 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Modelscited by 8,851
  2. 2023A Survey of Large Language Modelscited by 2,537
  3. 2024OlympiadBench: A Challenging Benchmark for Promoting AGI with Olympiad-Level Bilingual Multimodal Scientific Problemscited by 1,099
  4. 2024Large Language Monkeys: Scaling Inference Compute with Repeated Samplingcited by 946
  5. 2023Large Language Modelscited by 774
  6. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  7. 2023Llemma: An Open Language Model For Mathematicscited by 385
  8. 2024Large Language Models for Mathematical Reasoning: Progresses and Challengescited by 283
  9. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  10. 2024Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Modelscited by 277
  11. 2025MathArena: Evaluating LLMs on Uncontaminated Math Competitionscited by 275
  12. 2022Autoformalization with Large Language Modelscited by 252
38 more
  1. 2024FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AIcited by 227
  2. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  3. 2025A Survey on Test-Time Scaling in Large Language Models: What, How, Where, and How Well?cited by 215
  4. 2025The Landscape of Agentic Reinforcement Learning for LLMs: A Surveycited by 195
  5. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  6. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  7. 2025Reasoning Models Can Be Effective Without Thinkingcited by 182
  8. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  9. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 173
  10. 2024GSM-Plus: A Comprehensive Benchmark for Evaluating the Robustness of LLMs as Mathematical Problem Solverscited by 155
  11. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 153
  12. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  13. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
  14. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  15. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
  16. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  17. 2024InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoningcited by 117
  18. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
  19. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  20. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 97
  21. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Provingcited by 96
  22. 2024DART-Math: Difficulty-Aware Rejection Tuning for Mathematical Problem-Solvingcited by 92
  23. 2025CWM: An Open-Weights LLM for Research on Code Generation with World Modelscited by 87
  24. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 82
  25. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  26. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 78
  27. 2025Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpeningcited by 78
  28. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 77
  29. 2023Have LLMs Advanced Enough? A Challenging Problem Solving Benchmark For Large Language Modelscited by 76
  30. 2025Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiadcited by 72
  31. 2025Towards Robust Mathematical Reasoningcited by 67
  32. 2024Building Math Agents with Multi-Turn Iterative Preference Learningcited by 66
  33. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 64
  34. 2022Parsel: Algorithmic Reasoning with Language Models by Composing Decompositionscited by 62
  35. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Expertscited by 58
  36. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  37. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 55
  38. 2023FIMO: A Challenge Formal Dataset for Automated Theorem Provingcited by 54

50 most cited of 380 All 380 (JSON)