mlsanityData to 7 Oct 2026

ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics

arXiv 2302.12433 ↗First posted 24 Feb 2023cs.CL cs.AI cs.LOcited by 180

Not on the map. Why?

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

Abstract (arXiv)

We introduce ProofNet, a benchmark for autoformalization and formal proving of undergraduate-level mathematics. The ProofNet benchmarks consists of 371 examples, each consisting of a formal theorem statement in Lean 3, a natural language theorem statement, and a natural language proof. The problems are primarily drawn from popular undergraduate pure mathematics textbooks and cover topics such as real and complex analysis, linear algebra, abstract algebra, and topology. We intend for ProofNet to be a challenging benchmark that will drive progress in autoformalization and automatic theorem proving. We report baseline results on statement autoformalization via in-context learning. Moreover, we introduce two novel statement autoformalization methods: prompt retrieval and distilled backtranslation.

Key facts. Cited by 180 papers in the map (data through 7 Oct 2026). Builds on 25 of its 39 references that are in the map. First posted on arXiv 24 Feb 2023.

Builds on

25 of 39 references.

References · 25

  1. 2020Language Models are Few-Shot Learnerscited by 32,199
  2. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  3. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,203
  4. 2022Large Language Models are Zero-Shot Reasonerscited by 4,323
  5. 2019The Curious Case of Neural Text Degenerationcited by 2,881
  6. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,359
  7. 2017Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithmcited by 723
  8. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  9. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  10. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  11. 2017Unsupervised Machine Translation Using Monolingual Corpora Onlycited by 272
  12. 2022Autoformalization with Large Language Modelscited by 252
13 more
  1. 2022Memorizing Transformerscited by 219
  2. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  3. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  4. 2019The Lean mathematical librarycited by 127
  5. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  6. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 97
  7. 2023The unreasonable effectiveness of few-shot learning for machine translationcited by 91
  8. 2016DeepMath - Deep Sequence Models for Premise Selectioncited by 80
  9. 2021NaturalProofs: Mathematical Theorem Proving in Natural Languagecited by 80
  10. 2022NaturalProver: Grounded Mathematical Proof Generation with Language Modelscited by 72
  11. 2018First Experiments with Neural Translation of Informal to Formal Mathematicscited by 52
  12. 2021Unsupervised Neural Machine Translation with Generative Language Models Onlycited by 24
  13. 2019Formalising perfectoid spacescited by 7

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2023: 15; 2024: 27; 2025: 75; 2026: 63.

180 papers.

Sort:

By area:

  1. 2023A Survey of Large Language Modelscited by 2,537
  2. 2023Large Language Modelscited by 774
  3. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  4. 2023Llemma: An Open Language Model For Mathematicscited by 385
  5. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 270
  6. 2025The Landscape of Agentic Reinforcement Learning for LLMs: A Surveycited by 195
  7. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  8. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 173
  9. 2023LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Proverscited by 161
  10. 2023OpenWebMath: An Open Dataset of High-Quality Mathematical Web Textcited by 151
  11. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
  12. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
38 more
  1. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
  2. 2025CWM: An Open-Weights LLM for Research on Code Generation with World Modelscited by 87
  3. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  4. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 77
  5. 2023MathPile: A Billion-Token-Scale Pretraining Corpus for Mathcited by 67
  6. 2025Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Modelscited by 65
  7. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 64
  8. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Expertscited by 58
  9. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  10. 2024Herald: A Natural Language Annotated Lean 4 Datasetcited by 54
  11. 2024Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalizationcited by 53
  12. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 52
  13. 2024MathOdyssey: Benchmarking Mathematical Problem-Solving Skills in Large Language Models Using Odyssey Math Datacited by 51
  14. 2024Process-Driven Autoformalization in Lean 4cited by 45
  15. 2025FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Modelscited by 45
  16. 2023Multilingual Mathematical Autoformalizationcited by 38
  17. 2023Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Provingcited by 37
  18. 2024miniCTX: Neural Theorem Proving with (Long-)Contextscited by 35
  19. 2025Nemotron-CC-Math: A 133 Billion-Token-Scale High Quality Math Pretraining Datasetcited by 34
  20. 2025Theoretical Physics Benchmark (TPBench) -- a Dataset and Study of AI Reasoning Capabilities in Theoretical Physicscited by 33
  21. 2025CombiBench: Benchmarking LLM Capability for Combinatorial Mathematicscited by 28
  22. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 28
  23. 2024Autoformalizing Euclidean Geometrycited by 27
  24. 2024Autonomous Data Selection with Zero-shot Generative Classifiers for Mathematical Textscited by 26
  25. 2025Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learningcited by 26
  26. 2023Lyra: Orchestrating Dual Correction in Automated Theorem Provingcited by 24
  27. 2023Mathematical Language Models: A Surveycited by 24
  28. 2024U-MATH: A University-Level Benchmark for Evaluating Mathematical Skills in LLMscited by 24
  29. 2025ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Datacited by 23
  30. 2025ShadowCoT: Cognitive Hijacking for Stealthy Reasoning Backdoors in LLMscited by 23
  31. 2024Consistent Autoformalization for Constructing Mathematical Librariescited by 20
  32. 2025Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitionscited by 20
  33. 2024FormalAlign: Automated Alignment Evaluation for Autoformalizationcited by 19
  34. 2025REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoningcited by 18
  35. 2025Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Modelscited by 18
  36. 2025Towards Concise and Adaptive Thinking in Large Reasoning Models: A Surveycited by 18
  37. 2025Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graphcited by 18
  38. 2025ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimizationcited by 18

50 most cited of 180 All 180 (JSON)