# Learning to Prove Theorems by Learning to Generate Theorems

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

## Key facts

- Cited by 43 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Feb 2020.

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

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Explaining Answers with Entailment Trees](https://mlsanity.com/paper/2104.08661/) (2021)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [NaturalProofs: Mathematical Theorem Proving in Natural Language](https://mlsanity.com/paper/2104.01112/) (2021)
- [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025)
- [Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://mlsanity.com/paper/2404.12534/) (2024)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Learning Formal Mathematics From Intrinsic Motivation](https://mlsanity.com/paper/2407.00695/) (2024)
- [MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data](https://mlsanity.com/paper/2402.08957/) (2024)
- [Forward-Backward Reasoning in Large Language Models for Mathematical Verification](https://mlsanity.com/paper/2308.07758/) (2023)
- [LeanAgent: Lifelong Learning for Formal Theorem Proving](https://mlsanity.com/paper/2410.06209/) (2024)
- [Solving Formal Math Problems by Decomposition and Iterative Reflection](https://mlsanity.com/paper/2507.15225/) (2025)
- [CodeIt: Self-Improving Language Models with Prioritized Hindsight Replay](https://mlsanity.com/paper/2402.04858/) (2024)
- [Consistent Autoformalization for Constructing Mathematical Libraries](https://mlsanity.com/paper/2410.04194/) (2024)
- [Can neural networks do arithmetic? A survey on the elementary numerical skills of state-of-the-art deep learning models](https://mlsanity.com/paper/2303.07735/) (2023)
- [Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4](https://mlsanity.com/paper/2410.16429/) (2024)
- [Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving](https://mlsanity.com/paper/2404.07382/) (2024)
- [A Survey in Mathematical Language Processing](https://mlsanity.com/paper/2205.15231/) (2022)
- [Abstract Visual Reasoning: An Algebraic Approach for Solving Raven's Progressive Matrices](https://mlsanity.com/paper/2303.11730/) (2023)
- [REFACTOR: Learning to Extract Theorems from Proofs](https://mlsanity.com/paper/2402.17032/) (2024)
- [Training a First-Order Theorem Prover from Synthetic Data](https://mlsanity.com/paper/2103.03798/) (2021)
- [Can Transformers Do Enumerative Geometry?](https://mlsanity.com/paper/2408.14915/) (2024)
- [Lean Finder: Semantic Search for Mathlib That Understands User Intents](https://mlsanity.com/paper/2510.15940/) (2025)
- [Teaching Probabilistic Logical Reasoning to Transformers](https://mlsanity.com/paper/2305.13179/) (2023)
- [Learning to Compute Gr"obner Bases](https://mlsanity.com/paper/2311.12904/) (2023)
- [ATG: Benchmarking Automated Theorem Generation for Generative Language Models](https://mlsanity.com/paper/2405.06677/) (2024)
- [3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes](https://mlsanity.com/paper/2410.11133/) (2024)

## Abstract (arXiv)

We consider the task of automated theorem proving, a key AI task. Deep learning has shown promise for training theorem provers, but there are limited human-written theorems and proofs available for supervised learning. To address this limitation, we propose to learn a neural generator that automatically synthesizes theorems and proofs for the purpose of training a theorem prover. Experiments on real-world tasks demonstrate that synthetic data from our approach improves the theorem prover and advances the state of the art of automated theorem proving in Metamath. Code is available at https://github.com/princeton-vl/MetaGen.