In this paper, we present a novel and interesting method for automatically guessing lemmas, in order to improve the performance of automatic lemmas and lower the entry barrier for formalizing mathematics in proof aids. To overcome the limitations of existing neural networks and symbolic approaches, we propose a novel neural symbolic lemma guesser, Lemmanaid, which combines large-scale language models (LLMs) and symbolic methods. Lemmanaid generates templates describing the form of lemmas using LLMs and fills in the details using symbolic methods. Using the proof library of the Isabelle proof aid, we compare Lemmanaid with LLMs trained to generate complete lemma sentences and existing fully symbolic guessing methods. As a result, Lemmanaid outperforms existing methods on the test set of Isabelle’s HOL library and formal proof archive, and discovers 29-39.5% of the gold standard lemmas written by humans, which is 8-15% more lemmas than pure neural network methods. This study promotes computer-aided theory development and formalization by combining the strengths of neural networks and symbolic methods to generate useful auxiliary theorems for a variety of input domains.
