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.

翻译：注意到引理是数学中的一个关键特征，我们对引理在自动定理证明中的作用进行了研究。本文描述了一个结合学习技术的组合系统的实验，该系统为自动定理证明器生成有用的引理，展示了在多个代表性系统中的改进，并解决了一个二十年来未被任何系统解决的难题。通过聚焦于压缩分离问题，我们大幅简化了设置，从而得以触及引理及其在证明搜索中的本质作用。