Lemmanaid: Neuro-Symbolic Lemma Conjecturing
Yousef Alhessi, Sólrún Halla Einarsdóttir, George Granberry, Emily First, Moa Johansson, Sorin Lerner, Nicholas Smallbone
TL;DR
Lemmanaid introduces a novel neuro-symbolic approach to conjecturing lemmas by analogy across formal theories, leveraging a fine-tuned language model to generate lemma templates and a symbolic engine to instantiate them in Isabelle/HOL libraries. By evaluating on Isabelle/HOL and AFP benchmarks, and comparing against neural baselines and QuickSpec, Lemmanaid achieves superior coverage of gold-standard lemmas and benefits from ensemble strategies, with notable performance in the Octonions case study. The work demonstrates the value of bottom-up conjecturing via templates, providing a scalable path toward augmenting formal libraries and supporting automated theorem proving. It also highlights opportunities to integrate conjecturing with auto-formalization workflows and future enhancements to template instantiation and template design under computational constraints.
Abstract
Mathematicians and computer scientists are increasingly using proof assistants to formalize and check correctness of complex proofs. This is a non-trivial task in itself, however, with high demands on human expertise. Can we lower the bar by introducing automation for conjecturing 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 complete lemma statements (a purely neural method), as well as a fully symbolic conjecturing method. LEMMANAID consistently outperforms both neural and symbolic methods on test sets from Isabelle's HOL library and from its Archive of Formal Proofs (AFP). Using DeepSeek-coder-6.7B as a backend, LEMMANAID discovers 50% (HOL) and 28% (AFP) of the gold standard reference lemmas, 8-13% more than the corresponding neural-only method. Ensembling two LEMMANAID versions with different prompting strategies further increases performance to 55% and 34% respectively. In a case study on the formalization of 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. Our result show that LEMMANAID is able to conjecture a significant number of interesting lemmas across a wide range of domains covering formalizations over complex concepts in both mathematics and computer science, going far beyond the basic concepts of standard benchmarks such as miniF2F, PutnamBench and ProofNet.