mlsanityData to 7 Oct 2026

NaturalProofs: Mathematical Theorem Proving in Natural Language

arXiv 2104.01112 ↗First posted 24 Mar 2021cs.IR cs.LGcited by 80

Not on the map. Why?

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

Abstract (arXiv)

Understanding and creating mathematics using natural mathematical language - the mixture of symbolic and natural language used by humans - is a challenging and important problem for driving progress in machine learning. As a step in this direction, we develop NaturalProofs, a multi-domain corpus of mathematical statements and their proofs, written in natural mathematical language. NaturalProofs unifies broad coverage, deep coverage, and low-resource mathematical sources, allowing for evaluating both in-distribution and zero-shot generalization. Using NaturalProofs, we benchmark strong neural methods on mathematical reference retrieval and generation tasks which test a system's ability to determine key results that appear in a proof. Large-scale sequence models show promise compared to classical information retrieval methods, yet their performance and out-of-domain generalization leave substantial room for improvement. NaturalProofs opens many avenues for research on challenging mathematical tasks.

Key facts. Cited by 80 papers in the map (data through 7 Oct 2026). Builds on 34 of its 70 references that are in the map. First posted on arXiv 24 Mar 2021.

Builds on

34 of 70 references.

References · 34

  1. 2018BERT: Pre-training of Deep Bidirectional Transformers for Language Understandingcited by 40,204
  2. 2020Language Models are Few-Shot Learnerscited by 32,199
  3. 2019Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformercited by 14,491
  4. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,203
  5. 2020Dense Passage Retrieval for Open-Domain Question Answeringcited by 3,779
  6. 2017A Broad-Coverage Challenge Corpus for Sentence Understanding through Inferencecited by 2,665
  7. 2019Language Models as Knowledge Bases?cited by 1,922
  8. 2020XTREME: A Massively Multilingual Multi-task Benchmark for Evaluating Cross-lingual Generalizationcited by 738
  9. 2019MathQA: Towards Interpretable Math Word Problem Solving with Operation-Based Formalismscited by 653
  10. 2017Program Induction by Rationale Generation : Learning to Solve and Explain Algebraic Word Problemscited by 642
  11. 2019Passage Re-ranking with BERTcited by 629
  12. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
22 more
  1. 2016Solving General Arithmetic Word Problemscited by 353
  2. 2019Analysing Mathematical Reasoning Abilities of Neural Modelscited by 331
  3. 2020ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Languagecited by 309
  4. 2020Pretrained Transformers Improve Out-of-Distribution Robustnesscited by 293
  5. 2019Deep Learning for Symbolic Mathematicscited by 266
  6. 2020Transformers as Soft Reasoners over Languagecited by 265
  7. 2019Leveraging Pre-trained Checkpoints for Sequence Generation Taskscited by 182
  8. 2020Adversarial Filters of Dataset Biasescited by 159
  9. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  10. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  11. 2018The Dataset Nutrition Label: A Framework To Drive Higher Data Quality Standardscited by 97
  12. 2016DeepMath - Deep Sequence Models for Premise Selectioncited by 80
  13. 2018GamePad: A Learning Environment for Theorem Provingcited by 48
  14. 2021LIME: Learning Inductive Bias for Primitives of Mathematical Reasoningcited by 46
  15. 2020Learning to Prove Theorems by Learning to Generate Theoremscited by 43
  16. 2019Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizarcited by 40
  17. 2016Holophrasm: a neural Automated Theorem Prover for higher-order logiccited by 29
  18. 2020Beyond [CLS] through Ranking by Generationcited by 20
  19. 2019HOList: An Environment for Machine Learning of Higher-Order Theorem Provingcited by 19
  20. 2020Natural Language Premise Selection: Finding Supporting Statements for Mathematical Textcited by 13
  21. 2020Document-Level Definition Detection in Scholarly Documents: Existing Models, Error Analyses, and Future Directionscited by 11
  22. 2017Loss Functions for Multiset Predictioncited by 6

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2021: 1; 2022: 12; 2023: 19; 2024: 15; 2025: 22; 2026: 11.

80 papers.

Sort:

By area:

  1. 2023A Survey of Large Language Modelscited by 2,537
  2. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,359
  3. 2024OlympiadBench: A Challenging Benchmark for Promoting AGI with Olympiad-Level Bilingual Multimodal Scientific Problemscited by 1,099
  4. 2023Large Language Modelscited by 774
  5. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  6. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  7. 2022Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thoughtcited by 334
  8. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  9. 2023Mathematical Capabilities of ChatGPTcited by 263
  10. 2023Can Language Models Solve Graph Problems in Natural Language?cited by 249
  11. 2023SciBench: Evaluating College-Level Scientific Problem-Solving Abilities of Large Language Modelscited by 246
  12. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
38 more
  1. 2023OpenWebMath: An Open Dataset of High-Quality Mathematical Web Textcited by 151
  2. 2022UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expressioncited by 137
  3. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
  4. 2022Teaching Algorithmic Reasoning via In-context Learningcited by 111
  5. 2022On the Paradox of Learning to Reason from Datacited by 93
  6. 2024The BiGGen Bench: A Principled Benchmark for Fine-grained Evaluation of Language Models with Language Modelscited by 89
  7. 2023ReCEval: Evaluating Reasoning Chains via Correctness and Informativenesscited by 76
  8. 2022NaturalProver: Grounded Mathematical Proof Generation with Language Modelscited by 72
  9. 2023MathPile: A Billion-Token-Scale Pretraining Corpus for Mathcited by 67
  10. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 64
  11. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  12. 2024DafnyBench: A Benchmark for Formal Software Verificationcited by 54
  13. 2024Scaling Retrieval-Based Language Models with a Trillion-Token Datastorecited by 54
  14. 2025A Survey on Large Language Models for Mathematical Reasoningcited by 52
  15. 2025Nemotron-CC-Math: A 133 Billion-Token-Scale High Quality Math Pretraining Datasetcited by 34
  16. 2024Are Large Language Models Good Statisticians?cited by 26
  17. 2023Lyra: Orchestrating Dual Correction in Automated Theorem Provingcited by 24
  18. 2023TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Modelscited by 24
  19. 2023Mathematical Language Models: A Surveycited by 24
  20. 2024Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchicallycited by 22
  21. 2025Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitionscited by 20
  22. 2025Proving the Coding Interview: A Benchmark for Formally Verified Code Generationcited by 18
  23. 2025ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalizationcited by 18
  24. 2022AbductionRules: Training Transformers to Explain Unexpected Inputscited by 17
  25. 2025From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofscited by 17
  26. 2025CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalizationcited by 15
  27. 2024MIND: Math Informed syNthetic Dialogues for Pretraining LLMscited by 14
  28. 2022Lila: A Unified Benchmark for Mathematical Reasoningcited by 13
  29. 2025A Survey on Mathematical Reasoning and Optimization with Large Language Modelscited by 12
  30. 2024Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Provingcited by 11
  31. 2024Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learningcited by 11
  32. 2025Decomposing Elements of Problem Solving: What "Math" Does RL Teach?cited by 10
  33. 2022A Survey in Mathematical Language Processingcited by 9
  34. 2023BERT is not The Count: Learning to Match Mathematical Statements with Proofscited by 9
  35. 2024Varying Shades of Wrong: Aligning LLMs with Wrong Answers Onlycited by 9
  36. 2025FormaRL: Enhancing Autoformalization with no Labeled Datacited by 9
  37. 2025Frustratingly Simple Retrieval Improves Challenging, Reasoning-Intensive Benchmarkscited by 8
  38. 2024Controllable Text Generation in the Instruction-Tuning Eracited by 7

50 most cited of 80 All 80 (JSON)