# NaturalProofs: Mathematical Theorem Proving in Natural Language

arXiv: https://arxiv.org/abs/2104.01112 · HTML: https://mlsanity.com/paper/2104.01112/

## Key facts

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

## Builds on (most cited first, 30 of 34)

- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformer](https://mlsanity.com/paper/1910.10683/) (2019)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Dense Passage Retrieval for Open-Domain Question Answering](https://mlsanity.com/paper/2004.04906/) (2020)
- [A Broad-Coverage Challenge Corpus for Sentence Understanding through Inference](https://mlsanity.com/paper/1704.05426/) (2017)
- [Language Models as Knowledge Bases?](https://mlsanity.com/paper/1909.01066/) (2019)
- [XTREME: A Massively Multilingual Multi-task Benchmark for Evaluating Cross-lingual Generalization](https://mlsanity.com/paper/2003.11080/) (2020)
- [MathQA: Towards Interpretable Math Word Problem Solving with Operation-Based Formalisms](https://mlsanity.com/paper/1905.13319/) (2019)
- [Program Induction by Rationale Generation : Learning to Solve and Explain Algebraic Word Problems](https://mlsanity.com/paper/1705.04146/) (2017)
- [Passage Re-ranking with BERT](https://mlsanity.com/paper/1901.04085/) (2019)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Solving General Arithmetic Word Problems](https://mlsanity.com/paper/1608.01413/) (2016)
- [Analysing Mathematical Reasoning Abilities of Neural Models](https://mlsanity.com/paper/1904.01557/) (2019)
- [ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language](https://mlsanity.com/paper/2012.13048/) (2020)
- [Pretrained Transformers Improve Out-of-Distribution Robustness](https://mlsanity.com/paper/2004.06100/) (2020)
- [Deep Learning for Symbolic Mathematics](https://mlsanity.com/paper/1912.01412/) (2019)
- [Transformers as Soft Reasoners over Language](https://mlsanity.com/paper/2002.05867/) (2020)
- [Leveraging Pre-trained Checkpoints for Sequence Generation Tasks](https://mlsanity.com/paper/1907.12461/) (2019)
- [Adversarial Filters of Dataset Biases](https://mlsanity.com/paper/2002.04108/) (2020)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [The Dataset Nutrition Label: A Framework To Drive Higher Data Quality Standards](https://mlsanity.com/paper/1805.03677/) (2018)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [GamePad: A Learning Environment for Theorem Proving](https://mlsanity.com/paper/1806.00608/) (2018)
- [LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning](https://mlsanity.com/paper/2101.06223/) (2021)
- [Learning to Prove Theorems by Learning to Generate Theorems](https://mlsanity.com/paper/2002.07019/) (2020)
- [Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar](https://mlsanity.com/paper/1912.02636/) (2019)
- [Holophrasm: a neural Automated Theorem Prover for higher-order logic](https://mlsanity.com/paper/1608.02644/) (2016)
- [Beyond [CLS] through Ranking by Generation](https://mlsanity.com/paper/2010.03073/) (2020)

## Built on by (most cited first, 30 of 81)

- [A Survey of Large Language Models](https://mlsanity.com/paper/2303.18223/) (2023)
- [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022)
- [OlympiadBench: A Challenging Benchmark for Promoting AGI with Olympiad-Level Bilingual Multimodal Scientific Problems](https://mlsanity.com/paper/2402.14008/) (2024)
- [Large Language Models](https://mlsanity.com/paper/2307.05782/) (2023)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought](https://mlsanity.com/paper/2210.01240/) (2022)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Mathematical Capabilities of ChatGPT](https://mlsanity.com/paper/2301.13867/) (2023)
- [SciBench: Evaluating College-Level Scientific Problem-Solving Abilities of Large Language Models](https://mlsanity.com/paper/2307.10635/) (2023)
- [Can Language Models Solve Graph Problems in Natural Language?](https://mlsanity.com/paper/2305.10037/) (2023)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [OpenWebMath: An Open Dataset of High-Quality Mathematical Web Text](https://mlsanity.com/paper/2310.06786/) (2023)
- [UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expression](https://mlsanity.com/paper/2212.02746/) (2022)
- [A Survey of Deep Learning for Mathematical Reasoning](https://mlsanity.com/paper/2212.10535/) (2022)
- [Teaching Algorithmic Reasoning via In-context Learning](https://mlsanity.com/paper/2211.09066/) (2022)
- [On the Paradox of Learning to Reason from Data](https://mlsanity.com/paper/2205.11502/) (2022)
- [The BiGGen Bench: A Principled Benchmark for Fine-grained Evaluation of Language Models with Language Models](https://mlsanity.com/paper/2406.05761/) (2024)
- [ReCEval: Evaluating Reasoning Chains via Correctness and Informativeness](https://mlsanity.com/paper/2304.10703/) (2023)
- [NaturalProver: Grounded Mathematical Proof Generation with Language Models](https://mlsanity.com/paper/2205.12910/) (2022)
- [Lean-STaR: Learning to Interleave Thinking and Proving](https://mlsanity.com/paper/2407.10040/) (2024)
- [MathPile: A Billion-Token-Scale Pretraining Corpus for Math](https://mlsanity.com/paper/2312.17120/) (2023)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [Scaling Retrieval-Based Language Models with a Trillion-Token Datastore](https://mlsanity.com/paper/2407.12854/) (2024)
- [A Survey on Large Language Models for Mathematical Reasoning](https://mlsanity.com/paper/2506.08446/) (2025)
- [Nemotron-CC-Math: A 133 Billion-Token-Scale High Quality Math Pretraining Dataset](https://mlsanity.com/paper/2508.15096/) (2025)
- [Are Large Language Models Good Statisticians?](https://mlsanity.com/paper/2406.07815/) (2024)
- [Lyra: Orchestrating Dual Correction in Automated Theorem Proving](https://mlsanity.com/paper/2309.15806/) (2023)
- [TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models](https://mlsanity.com/paper/2310.10180/) (2023)

## 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.