# ATG: Benchmarking Automated Theorem Generation for Generative Language Models

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 23 of its 46 references that are in the map.
- First posted on arXiv 5 May 2024.

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

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Semi-Supervised Classification with Graph Convolutional Networks](https://mlsanity.com/paper/1609.02907/) (2016)
- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [Code Llama: Open Foundation Models for Code](https://mlsanity.com/paper/2308.12950/) (2023)
- [Neural Operator: Graph Kernel Network for Partial Differential Equations](https://mlsanity.com/paper/2003.03485/) (2020)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Unsupervised Translation of Programming Languages](https://mlsanity.com/paper/2006.03511/) (2020)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [Augmenting Operations Research with Auto-Formulation of Optimization Models from Problem Descriptions](https://mlsanity.com/paper/2209.15565/) (2022)
- [Premise Selection for Theorem Proving by Deep Graph Embedding](https://mlsanity.com/paper/1709.09994/) (2017)
- [INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving](https://mlsanity.com/paper/2007.02924/) (2020)
- [Learning to Prove Theorems by Learning to Generate Theorems](https://mlsanity.com/paper/2002.07019/) (2020)
- [Holophrasm: a neural Automated Theorem Prover for higher-order logic](https://mlsanity.com/paper/1608.02644/) (2016)
- [Machine learning and information theory concepts towards an AI Mathematician](https://mlsanity.com/paper/2403.04571/) (2024)
- [Linear programming word problems formulation using EnsembleCRF NER labeler and T5 text generator with data augmentations](https://mlsanity.com/paper/2212.14657/) (2022)

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

- [A Systematic Survey on Large Language Models for Algorithm Design](https://mlsanity.com/paper/2410.14716/) (2024)
- [Can Transformers Do Enumerative Geometry?](https://mlsanity.com/paper/2408.14915/) (2024)
- [Library Learning Doesn't: The Curious Case of the Single-Use "Library"](https://mlsanity.com/paper/2410.20274/) (2024)
- [A Compute-Matched Re-Evaluation of TroVE on MATH](https://mlsanity.com/paper/2507.22069/) (2025)
- [Artifical intelligence and inherent mathematical difficulty](https://mlsanity.com/paper/2408.03345/) (2024)
- [An Automated Theorem Generator with Theoretical Foundation Based on Rectangular Standard Contradiction](https://mlsanity.com/paper/2511.04092/) (2025)

## Abstract (arXiv)

Humans can develop new theorems to explore broader and more complex mathematical results. While current generative language models (LMs) have achieved significant improvement in automatically proving theorems, their ability to generate new or reusable theorems is still under-explored. Without the new theorems, current LMs struggle to prove harder theorems that are distant from the given hypotheses with the exponentially growing search space. Therefore, this paper proposes an Automated Theorem Generation (ATG) benchmark that evaluates whether an agent can automatically generate valuable (and possibly brand new) theorems that are applicable for downstream theorem proving as reusable knowledge. Specifically, we construct the ATG benchmark by splitting the Metamath library into three sets: axioms, library, and problem based on their proving depth. We conduct extensive experiments to investigate whether current LMs can generate theorems in the library and benefit the problem theorems proving. The results demonstrate that high-quality ATG data facilitates models' performances on downstream ATP. However, there is still room for current LMs to develop better ATG and generate more advanced and human-like theorems. We hope the new ATG challenge can shed some light on advanced complex theorem proving.