Mathematicians and computer scientists are increasingly leveraging proof assistants to formalize and check complex proofs, a task that demands substantial expertise. Can we lower the bar by automating the conjecturing of helpful, interesting and novel lemmas? We present the first neuro-symbolic lemma conjecturing tool, LEMMANAID, designed to discover conjectures by drawing analogies between mathematical theories. LEMMANAID uses a fine-tuned LLM to generate lemma templates that describe the shape of a lemma, and symbolic methods to fill in the details. We compare LEMMANAID against the same LLM fine-tuned to generate lemmas directly, as well as a fully symbolic conjecturing method. On test sets from Isabelle's HOL library and Archive of Formal Proofs (AFP), LEMMANAID consistently outperforms both neural and symbolic methods. Using DeepSeek-coder-6.7B as a backend, LEMMANAID discovers 50% (HOL) and 29% (AFP) of the gold standard lemmas, increasing to 55% and 35% when ensembling prompting strategies. In a case study on Octonions, LEMMANAID discovers 79% of the gold standard lemmas, compared to 62% for neural-only and 23% for the state of the art symbolic tool. Furthermore, in a targeted comparison, LEMMANAID discovers more gold standard lemmas than both Claude Opus 4.5 and GPT-5.2. Our results show that LEMMANAID can conjecture a significant number of interesting lemmas across complex formalizations in mathematics and computer science.

翻译：数学家和计算机科学家正越来越多地利用证明助手来形式化并验证复杂证明，这是一项需要大量专业知识的工作。我们能否通过自动化猜想那些有用、有趣且新颖的引理来降低门槛？我们提出了首个神经符号引理猜想工具LEMMANAID，旨在通过类比数学理论中的相似性来发现猜想。LEMMANAID使用经过微调的大型语言模型（LLM）生成描述引理形态的引理模板，并采用符号方法填充细节。我们将LEMMANAID与直接生成引理的同一微调LLM以及一种完全符号化的猜想方法进行了比较。在来自Isabelle的HOL库和形式化证明档案库（AFP）的测试集上，LEMMANAID在性能上始终优于纯神经方法和符号方法。使用DeepSeek-coder-6.7B作为后端，LEMMANAID发现了50%（HOL）和29%（AFP）的金标准引理，当采用集成提示策略时，这一比例提升至55%和35%。在对八元数的案例研究中，LEMMANAID发现了79%的金标准引理，而纯神经方法为62%，当前最先进的符号工具仅为23%。此外，在一项针对性比较中，LEMMANAID发现的引理数量超过了Claude Opus 4.5和GPT-5.2。我们的结果表明，LEMMANAID能够在数学和计算机科学的复杂形式化体系中猜想出大量有趣的引理。