Lemmas: Generation, Selection, Application

Michael Rawson, Christoph Wernhard, Zsolt Zombori, Wolfgang Bibel
3/10/2023
cs.LOcs.AI

No official code found. Best implementation: zsoltzombori/lemma (3 stars, last commit 2023-03-13).

Abstract

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.

View on arXivView PDF

Code Implementations(1)

zsoltzombori/lemmaCommunity100%

Using lemmas to aid automated theorem proving for Condensed Detachment Problems

30Shell, Prolog3 years ago

Similar Papers

Investigations into Proof Structures

84% match2023

LEGO-Prover: Neural Theorem Proving with Growing Libraries

81% match1 repo682026

Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving

80% match2025

Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs

79% match1 repo272025

Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code

79% match2024

Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving

78% match2025

Cite this paper

@article{rawson2023lemmas,
  title  = {Lemmas: Generation, Selection, Application},
  author = {Michael Rawson and Christoph Wernhard and Zsolt Zombori and Wolfgang Bibel},
  year   = {2023},
  eprint = {2303.05854},
  archivePrefix = {arXiv},
  url    = {http://arxiv.org/abs/2303.05854v2}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/2303.05854.svg)](https://codeofpaper.com/paper/2303.05854)

Discussion