mlsanityData to 14 Oct 2026

Lemmas: Generation, Selection, Application

arXiv 2303.05854 ↗First posted 10 Mar 2023cs.LO cs.AIcited by 3

Not on the map. Why?

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.

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

17 of 100 references.

References · 17

  1. 2015Deep Residual Learning for Image Recognitioncited by 52,096
  2. 2019PyTorch: An Imperative Style, High-Performance Deep Learning Librarycited by 20,305
  3. 2015Batch Normalization: Accelerating Deep Network Training by Reducing Internal Covariate Shiftcited by 7,005
  4. 2020Generative Language Modeling for Automated Theorem Provingcited by 388
  5. 2016DeepMath - Deep Sequence Models for Premise Selectioncited by 81
  6. 2018Reinforcement Learning of Theorem Provingcited by 69
  7. 2017Deep Network Guided Proof Searchcited by 47
  8. 2017Premise Selection for Theorem Proving by Deep Graph Embeddingcited by 44
  9. 2017ENIGMA: Efficient Learning-based Inference Guiding Machinecited by 26
  10. 2020First Neural Conjecturing Datasets and Experimentscited by 26
  11. 2019Guiding Inferences in Connection Tableau by Recurrent Neural Networkscited by 6
  12. 2020Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logiccited by 6
5 more
  1. 2014Learning-assisted Theorem Proving with Millions of Lemmascited by 5
  2. 2021Learning from Lukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)cited by 5
  3. 2022CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description)cited by 3
  4. 2022Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Provingcited by 2
  5. 2023Investigations into Proof Structurescited by 2

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2023: 1; 2024: 1; 2025: 0; 2026: 1.

3 papers.

  1. 2024REFACTOR: Learning to Extract Theorems from Proofscited by 9
  2. 2023Range-Restricted Interpolation through Clausal Tableauxcited by 0
  3. 2026Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Proverscited by 0