Discovering New Theorems via LLMs with In-Context Proof Learning in Lean
This work addresses the challenge of automated theorem discovery in formal mathematics, offering a novel method for generating and verifying new theorems, though it is incremental in advancing LLM capabilities beyond existing problem-solving.
The paper tackles the problem of enabling Large Language Models (LLMs) to discover novel mathematical theorems, rather than just solving existing problems, by proposing a Conjecturing-Proving Loop pipeline that generates and proves conjectures in Lean 4 format using in-context learning of proof strategies. The result includes rediscovering theorems from past mathematical papers that were not previously formalized, with at least one theorem unprovable by the LLM without in-context learning, demonstrating the effectiveness of this approach.
Large Language Models have demonstrated significant promise in formal theorem proving. However, previous works mainly focus on solving existing problems. In this paper, we focus on the ability of LLMs to find novel theorems. We propose Conjecturing-Proving Loop pipeline for automatically generating mathematical conjectures and proving them in Lean 4 format. A feature of our approach is that we generate and prove further conjectures with context including previously generated theorems and their proofs, which enables the generation of more difficult proofs by in-context learning of proof strategies without changing parameters of LLMs. We demonstrated that our framework rediscovered theorems with verification, which were published in past mathematical papers and have not yet formalized. Moreover, at least one of these theorems could not be proved by the LLM without in-context learning, even in natural language, which means that in-context learning was effective for neural theorem proving. The source code is available at https://github.com/auto-res/ConjecturingProvingLoop.