@inproceedings{kasaura-etal-2026-discovering,
title = "Discovering New Theorems via {LLM}s with In-Context Proof Learning in Lean",
author = "Kasaura, Kazumi and
Onda, Naoto and
Oriike, Yuta and
Taniguchi, Masaya and
Sannai, Akiyoshi and
Sonoda, Sho",
editor = "Yanaka, Hitomi and
Abzianidze, Lasha",
booktitle = "Proceedings of the 6th Workshop on Natural Language Meets Logic and Machine Learning ({NALOMA})",
month = aug,
year = "2026",
address = "Prague, Czechia",
publisher = "Association for Computational Linguistics",
url = "https://aclanthology.org/2026.naloma-1.5/",
pages = "40--49",
ISBN = "979-8-89176-389-0",
abstract = "Large Language Models (LLMs) have demonstrated significant promise in formal theorem proving.In this study, we investigate the ability of LLMs to discover novel theorems and produce verified proofs. We propose a pipeline called *Conjecturing-Proving Loop* (CPL), which iteratively generates mathematical conjectures and attempts to prove them in Lean 4.A key feature of CPL is that each iteration conditions the LLM on previously generated theorems and their formal proofs, enabling parameter-free improvement of proof strategies via in-context learning.We provide both theoretical and experimental evidence that CPL increases the discovery rate of hard-to-prove theorems compared to frameworks that generate statements and proofs simultaneously.Moreover, our experiments show that reusing the LLM{'}s own formally verified outputs as context consistently improves subsequent proof success, demonstrating the effectiveness of self-generated in-context learning for neural theorem proving."
}<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="kasaura-etal-2026-discovering">
<titleInfo>
<title>Discovering New Theorems via LLMs with In-Context Proof Learning in Lean</title>
</titleInfo>
<name type="personal">
<namePart type="given">Kazumi</namePart>
<namePart type="family">Kasaura</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Naoto</namePart>
<namePart type="family">Onda</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Yuta</namePart>
<namePart type="family">Oriike</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Masaya</namePart>
<namePart type="family">Taniguchi</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Akiyoshi</namePart>
<namePart type="family">Sannai</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Sho</namePart>
<namePart type="family">Sonoda</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<originInfo>
<dateIssued>2026-08</dateIssued>
</originInfo>
<typeOfResource>text</typeOfResource>
<relatedItem type="host">
<titleInfo>
<title>Proceedings of the 6th Workshop on Natural Language Meets Logic and Machine Learning (NALOMA)</title>
</titleInfo>
<name type="personal">
<namePart type="given">Hitomi</namePart>
<namePart type="family">Yanaka</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Lasha</namePart>
<namePart type="family">Abzianidze</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<originInfo>
<publisher>Association for Computational Linguistics</publisher>
<place>
<placeTerm type="text">Prague, Czechia</placeTerm>
</place>
</originInfo>
<genre authority="marcgt">conference publication</genre>
<identifier type="isbn">979-8-89176-389-0</identifier>
</relatedItem>
<abstract>Large Language Models (LLMs) have demonstrated significant promise in formal theorem proving.In this study, we investigate the ability of LLMs to discover novel theorems and produce verified proofs. We propose a pipeline called *Conjecturing-Proving Loop* (CPL), which iteratively generates mathematical conjectures and attempts to prove them in Lean 4.A key feature of CPL is that each iteration conditions the LLM on previously generated theorems and their formal proofs, enabling parameter-free improvement of proof strategies via in-context learning.We provide both theoretical and experimental evidence that CPL increases the discovery rate of hard-to-prove theorems compared to frameworks that generate statements and proofs simultaneously.Moreover, our experiments show that reusing the LLM’s own formally verified outputs as context consistently improves subsequent proof success, demonstrating the effectiveness of self-generated in-context learning for neural theorem proving.</abstract>
<identifier type="citekey">kasaura-etal-2026-discovering</identifier>
<location>
<url>https://aclanthology.org/2026.naloma-1.5/</url>
</location>
<part>
<date>2026-08</date>
<extent unit="page">
<start>40</start>
<end>49</end>
</extent>
</part>
</mods>
</modsCollection>
%0 Conference Proceedings
%T Discovering New Theorems via LLMs with In-Context Proof Learning in Lean
%A Kasaura, Kazumi
%A Onda, Naoto
%A Oriike, Yuta
%A Taniguchi, Masaya
%A Sannai, Akiyoshi
%A Sonoda, Sho
%Y Yanaka, Hitomi
%Y Abzianidze, Lasha
%S Proceedings of the 6th Workshop on Natural Language Meets Logic and Machine Learning (NALOMA)
%D 2026
%8 August
%I Association for Computational Linguistics
%C Prague, Czechia
%@ 979-8-89176-389-0
%F kasaura-etal-2026-discovering
%X Large Language Models (LLMs) have demonstrated significant promise in formal theorem proving.In this study, we investigate the ability of LLMs to discover novel theorems and produce verified proofs. We propose a pipeline called *Conjecturing-Proving Loop* (CPL), which iteratively generates mathematical conjectures and attempts to prove them in Lean 4.A key feature of CPL is that each iteration conditions the LLM on previously generated theorems and their formal proofs, enabling parameter-free improvement of proof strategies via in-context learning.We provide both theoretical and experimental evidence that CPL increases the discovery rate of hard-to-prove theorems compared to frameworks that generate statements and proofs simultaneously.Moreover, our experiments show that reusing the LLM’s own formally verified outputs as context consistently improves subsequent proof success, demonstrating the effectiveness of self-generated in-context learning for neural theorem proving.
%U https://aclanthology.org/2026.naloma-1.5/
%P 40-49
Markdown (Informal)
[Discovering New Theorems via LLMs with In-Context Proof Learning in Lean](https://aclanthology.org/2026.naloma-1.5/) (Kasaura et al., NALOMA 2026)
ACL