mlsanityData to 7 Oct 2026

FIMO: A Challenge Formal Dataset for Automated Theorem Proving

arXiv 2309.04295 ↗First posted 8 Sep 2023cs.AIcited by 54

Not on the map. Why?

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

Abstract (arXiv)

We present FIMO, an innovative dataset comprising formal mathematical problem statements sourced from the International Mathematical Olympiad (IMO) Shortlisted Problems. Designed to facilitate advanced automated theorem proving at the IMO level, FIMO is currently tailored for the Lean formal language. It comprises 149 formal problem statements, accompanied by both informal problem descriptions and their corresponding LaTeX-based informal proofs. Through initial experiments involving GPT-4, our findings underscore the existing limitations in current methodologies, indicating a substantial journey ahead before achieving satisfactory IMO-level automated theorem proving outcomes.

Key facts. Cited by 54 papers in the map (data through 7 Oct 2026). Builds on 13 of its 16 references that are in the map. First posted on arXiv 8 Sep 2023.

Builds on

13 of 16 references.

References · 13

  1. 2020Language Models are Few-Shot Learnerscited by 32,199
  2. 2023GPT-4 Technical Reportcited by 18,132
  3. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,203
  4. 2023Reflexion: Language Agents with Verbal Reinforcement Learningcited by 4,064
  5. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  6. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  7. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  8. 2022Autoformalization with Large Language Modelscited by 252
  9. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  10. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  11. 2019The Lean mathematical librarycited by 127
  12. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 97
1 more
  1. 2021Generate & Rank: A Multi-task Framework for Math Word Problemscited by 82

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2023: 4; 2024: 15; 2025: 24; 2026: 11.

54 papers.

Sort:

By area:

  1. 2025MathArena: Evaluating LLMs on Uncontaminated Math Competitionscited by 275
  2. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  3. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
  4. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
  5. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  6. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  7. 2025Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiadcited by 72
  8. 2024OlympicArena: Benchmarking Multi-discipline Cognitive Reasoning for Superintelligent AIcited by 70
  9. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  10. 2025Satori: Reinforcement Learning with Chain-of-Action-Thought Enhances LLM Reasoning via Autoregressive Searchcited by 53
  11. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 52
  12. 2025LEXam: Benchmarking Legal Reasoning on 340 Law Examscited by 52
38 more
  1. 2024Process-Driven Autoformalization in Lean 4cited by 45
  2. 2025FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Modelscited by 45
  3. 2024MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Datacited by 43
  4. 2025Reasoning Language Models: A Blueprintcited by 41
  5. 2024miniCTX: Neural Theorem Proving with (Long-)Contextscited by 35
  6. 2024LeanAgent: Lifelong Learning for Formal Theorem Provingcited by 34
  7. 2024Proving Theorems Recursivelycited by 25
  8. 2023Lyra: Orchestrating Dual Correction in Automated Theorem Provingcited by 24
  9. 2023TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Modelscited by 24
  10. 2025DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learningcited by 23
  11. 2025FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levelscited by 23
  12. 2024Proving Olympiad Algebraic Inequalities without Human Demonstrationscited by 20
  13. 2024FormalAlign: Automated Alignment Evaluation for Autoformalizationcited by 19
  14. 2025Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Modelscited by 18
  15. 2025Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verificationcited by 16
  16. 2025CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalizationcited by 15
  17. 2025Reliable Fine-Grained Evaluation of Natural Language Math Proofscited by 14
  18. 2023Adapting Large Language Models for Education: Foundational Capabilities, Potentials, and Challengescited by 13
  19. 2024Integrating Intent Understanding and Optimal Behavior Planning for Behavior Tree Generation from Human Instructionscited by 12
  20. 2025Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Taskscited by 9
  21. 2024A Hybrid RAG System with Comprehensive Enhancement on Complex Reasoningcited by 8
  22. 2026LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematicscited by 7
  23. 2025LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)cited by 4
  24. 2025LemmaHead: RAG Assisted Proof Generation Using Large Language Modelscited by 3
  25. 2025IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touchcited by 3
  26. 2026The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statementscited by 3
  27. 2026Theory-Scale Auto-Formalization of Logics for Computer Sciencecited by 3
  28. 2025Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solvingcited by 2
  29. 2025MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verificationcited by 2
  30. 2025MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classificationcited by 2
  31. 2026Learning to Reason with Insight for Informal Theorem Provingcited by 2
  32. 2026FormalRx: Rectify and eXamine Semantic Failures in Autoformalizationcited by 2
  33. 2025Hierarchical Attention Generates Better Proofscited by 1
  34. 2025Formally Solving Answer-Construction Problems in Leancited by 1
  35. 2025Putnam-like dataset summary: LLMs as mathematical competition contestantscited by 1
  36. 2026Beyond Accuracy: Evaluating Strategy Diversity in LLM Mathematical Reasoningcited by 1
  37. 2025Max It or Miss It: Benchmarking LLM On Solving Extremal Problemscited by 0
  38. 2026MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Librariescited by 0

50 most cited of 54 All 54 (JSON)