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.

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