# Training a First-Order Theorem Prover from Synthetic Data

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 28 references that are in the map.
- First posted on arXiv 5 Mar 2021.

## Builds on (most cited first, 14 of 14)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Scaling Laws for Neural Language Models](https://mlsanity.com/paper/2001.08361/) (2020)
- [A Generalization of Transformer Networks to Graphs](https://mlsanity.com/paper/2012.09699/) (2020)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Emergent Complexity and Zero-shot Transfer via Unsupervised Environment Design](https://mlsanity.com/paper/2012.02096/) (2020)
- [Intrinsic Motivation and Automatic Curricula via Asymmetric Self-Play](https://mlsanity.com/paper/1703.05407/) (2017)
- [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)
- [Intrinsically Motivated Goal Exploration Processes with Automatic Curriculum Learning](https://mlsanity.com/paper/1708.02190/) (2017)
- [Deep Network Guided Proof Search](https://mlsanity.com/paper/1701.06972/) (2017)
- [Learning to Prove Theorems by Learning to Generate Theorems](https://mlsanity.com/paper/2002.07019/) (2020)
- [Automated curricula through setter-solver interactions](https://mlsanity.com/paper/1909.12892/) (2019)
- [HOList: An Environment for Machine Learning of Higher-Order Theorem Proving](https://mlsanity.com/paper/1904.03241/) (2019)

## Built on by (most cited first, 8 of 8)

- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Proposing and solving olympiad geometry with guided tree search](https://mlsanity.com/paper/2412.10673/) (2024)
- [Proving Theorems using Incremental Learning and Hindsight Experience Replay](https://mlsanity.com/paper/2112.10664/) (2021)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)
- [Adversarial Learning to Reason in an Arbitrary Logic](https://mlsanity.com/paper/2204.02737/) (2022)
- [Learning Better Representations From Less Data For Propositional Satisfiability](https://mlsanity.com/paper/2402.08365/) (2024)
- [Towards Generating Controllable and Solvable Geometry Problem by Leveraging Symbolic Deduction Engine](https://mlsanity.com/paper/2506.02565/) (2025)

## Abstract (arXiv)

A major challenge in applying machine learning to automated theorem proving is the scarcity of training data, which is a key ingredient in training successful deep learning models. To tackle this problem, we propose an approach that relies on training purely with synthetically generated theorems, without any human data aside from axioms. We use these theorems to train a neurally-guided saturation-based prover. Our neural prover outperforms the state-of-the-art E-prover on this synthetic data in both time and search steps, and shows significant transfer to the unseen human-written theorems from the TPTP library, where it solves 72% of first-order problems without equality.