Generating Theorems by Generating Proof Structures
Logic in Computer Science
2026-02-18 v1
Abstract
We address generating theorems from a given set of axioms, without proof goal, aiming at value from a mathematical point of view or as lemmas for automated proving. As benchmark, we convert a fragment of the Metamath database set.mm. Our techniques are centered on proof terms and condensed detachment, which ties in with approaches to automated first-order proving by proof structure enumeration, and links to Metamath as well as to formulas-as-types. Our methods for generating theorems are based on partitioning the set of proof terms into inductively characterized levels. We study two ideas for improvement: Lemma synthesis by DAG compression of proof term sets and incorporating combinators into proof term construction.
Cite
@article{arxiv.2602.15511,
title = {Generating Theorems by Generating Proof Structures},
author = {Christoph Wernhard},
journal= {arXiv preprint arXiv:2602.15511},
year = {2026}
}