TLDR: A new AI system called “Conjecturing-Proving Loop” uses Large Language Models (LLMs) to automatically generate and prove novel mathematical theorems in Lean 4. By learning from previously proven theorems and their proofs (in-context learning), the system can tackle more complex problems and has successfully rediscovered research-level theorems, demonstrating an improved proof ability without retraining the LLMs.
Large Language Models (LLMs) have shown significant potential in the field of formal theorem proving, a domain where mathematical statements are rigorously verified. Traditionally, research in this area has focused on using LLMs to solve existing mathematical problems. However, a new study introduces an innovative approach that empowers LLMs to discover novel theorems, rather than just proving known ones.
The researchers, Kazumi Kasaura, Naoto Onda, Yuta Oriike, Masaya Taniguchi, Akiyoshi Sannai, and Sho Sonoda, propose a system called the “Conjecturing-Proving Loop.” This pipeline is designed to automatically generate mathematical conjectures and then prove them using the Lean 4 formal proof system. A key aspect of this method is its ability to learn proof strategies “in-context.” This means that as the system successfully generates and proves theorems, these new theorems and their proofs are added to a “library.” This growing library then serves as context for the LLM to generate and prove even more complex conjectures, all without needing to retrain the LLM’s parameters.
The Conjecturing-Proving Loop operates in distinct phases: a conjecturer (an LLM agent) proposes new mathematical statements, and a prover (another LLM agent) attempts to construct formal proofs for these statements. A Lean server is used to verify the syntax of conjectures and the correctness of proofs. If a conjecture is proven, it’s added to the library, enriching the context for future iterations. This separation of conjecturing and proving helps prevent the system from getting stuck on similar types of theorems and encourages the exploration of more challenging mathematical ideas.
In their experiments, the team focused on minor topological notions like semi-openness, alpha-openness, and preopenness, which are defined within Lean’s mathematical library, Mathlib, but are not yet formally included. The goal was to see if their framework could rediscover important properties related to these notions. Remarkably, the system successfully rediscovered theorems that had been published in past mathematical papers but had not yet been formalized in Lean. One significant achievement was the rediscovery and proof of the theorem stating that “The intersection of two alpha-open sets is alpha-open.” This particular theorem is known to be a difficult part of proving that alpha-open sets form a topology.
A crucial finding from the study highlights the effectiveness of in-context learning. The researchers demonstrated that a theorem, which the LLM struggled to prove without the generated library as context (even in natural language), could be successfully proven when the context was provided. This suggests that the LLM learned effective proof strategies from the previously verified proofs it had generated itself, showcasing an improvement in its reasoning capabilities without explicit training.
The Conjecturing-Proving Loop framework not only rediscovered research-level theorems but also generated theorems with longer and more complex proofs compared to a baseline method that generated statements and proofs simultaneously. This indicates its potential for exploring deeper mathematical concepts. The source code for this innovative framework is publicly available, allowing other researchers to explore and build upon this work. You can find more details about this research in the full paper: Discovering New Theorems via LLMs with In-Context Proof Learning in Lean.
Also Read:
- Formalizing Advanced Algebraic Geometry: The Multi-Graded Proj Construction in Lean
- EconProver: Reducing Costs in Automated Theorem Proving
This work opens new avenues for the automatic expansion of formal mathematics libraries. By enabling AI to generate and prove novel propositions, it could significantly accelerate the formalization of mathematics, making complex mathematical theories more accessible and verifiable.
