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.

翻译：本文研究从给定公理集生成定理的方法，无需预设证明目标，旨在从数学角度创造价值或为自动证明提供引理。作为基准测试，我们转换了Metamath数据库set.mm的一个片段。我们的技术以证明项和压缩分离为核心，这与通过证明结构枚举实现一阶自动证明的方法相契合，同时关联到Metamath系统及公式即类型理论。我们通过将证明项集合划分为归纳特征化的层级来实现定理生成。我们研究了两种改进思路：通过证明项集合的DAG压缩进行引理合成，以及在证明项构造中引入组合子。