# Learning to Prove from Synthetic Theorems

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

## Key facts

- Cited by 13 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 19 Jun 2020.

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

- [Language Models Can Teach Themselves to Program Better](https://mlsanity.com/paper/2207.14502/) (2022)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [Open Source Vizier: Distributed Infrastructure and API for Reliable and Flexible Blackbox Optimization](https://mlsanity.com/paper/2207.13676/) (2022)
- [Learning to Guide a Saturation-Based Theorem Prover](https://mlsanity.com/paper/2106.03906/) (2021)
- [Proving Theorems using Incremental Learning and Hindsight Experience Replay](https://mlsanity.com/paper/2112.10664/) (2021)
- [Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis](https://mlsanity.com/paper/2205.14229/) (2022)
- [PhysNLU: A Language Resource for Evaluating Natural Language Understanding and Explanation Coherence in Physics](https://mlsanity.com/paper/2201.04275/) (2022)
- [Proving Equivalence Between Complex Expressions Using Graph-to-Sequence Neural Models](https://mlsanity.com/paper/2106.02452/) (2021)
- [Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem](https://mlsanity.com/paper/2509.06809/) (2025)
- [Learning to Prove Trigonometric Identities](https://mlsanity.com/paper/2207.06679/) (2022)
- [Hierarchical Attention Generates Better Proofs](https://mlsanity.com/paper/2504.19188/) (2025)
- [Generating Intermediate Steps for NLI with Next-Step Supervision](https://mlsanity.com/paper/2208.14641/) (2022)

## 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 with synthetic theorems, generated from a set of axioms. We show that such theorems can be used to train an automated prover and that the learned prover transfers successfully to human-generated theorems. We demonstrate that a prover trained exclusively on synthetic theorems can solve a substantial fraction of problems in TPTP, a benchmark dataset that is used to compare state-of-the-art heuristic provers. Our approach outperforms a model trained on human-generated problems in most axiom sets, thereby showing the promise of using synthetic data for this task.