# Lemmas: Generation, Selection, Application

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 17 of its 100 references that are in the map.
- First posted on arXiv 10 Mar 2023.

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

- [Deep Residual Learning for Image Recognition](https://mlsanity.com/paper/1512.03385/) (2015)
- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Batch Normalization: Accelerating Deep Network Training by Reducing Internal Covariate Shift](https://mlsanity.com/paper/1502.03167/) (2015)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [Deep Network Guided Proof Search](https://mlsanity.com/paper/1701.06972/) (2017)
- [Premise Selection for Theorem Proving by Deep Graph Embedding](https://mlsanity.com/paper/1709.09994/) (2017)
- [ENIGMA: Efficient Learning-based Inference Guiding Machine](https://mlsanity.com/paper/1701.06532/) (2017)
- [First Neural Conjecturing Datasets and Experiments](https://mlsanity.com/paper/2005.14664/) (2020)
- [Guiding Inferences in Connection Tableau by Recurrent Neural Networks](https://mlsanity.com/paper/1905.07961/) (2019)
- [Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic](https://mlsanity.com/paper/2002.10892/) (2020)
- [Learning-assisted Theorem Proving with Millions of Lemmas](https://mlsanity.com/paper/1402.3578/) (2014)
- [Learning from Lukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)](https://mlsanity.com/paper/2104.13645/) (2021)
- [CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description)](https://mlsanity.com/paper/2207.08453/) (2022)
- [Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving](https://mlsanity.com/paper/2209.12592/) (2022)
- [Investigations into Proof Structures](https://mlsanity.com/paper/2304.12827/) (2023)

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

- [REFACTOR: Learning to Extract Theorems from Proofs](https://mlsanity.com/paper/2402.17032/) (2024)
- [Range-Restricted Interpolation through Clausal Tableaux](https://mlsanity.com/paper/2306.03572/) (2023)
- [Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Provers](https://mlsanity.com/paper/2602.10512/) (2026)

## Abstract (arXiv)

Noting that lemmas are a key feature of mathematics, we engage in an investigation of the role of lemmas in automated theorem proving. The paper describes experiments with a combined system involving learning technology that generates useful lemmas for automated theorem provers, demonstrating improvement for several representative systems and solving a hard problem not solved by any system for twenty years. By focusing on condensed detachment problems we simplify the setting considerably, allowing us to get at the essence of lemmas and their role in proof search.