Discovering New Theorems via LLMs with In-Context Proof Learning in Lean

ArXi:2509.14274v2 Announce Type: replace-cross Large Language Models (LLMs) have nstrated 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 \textit{Conjecturing-Proving Loop} (CPL), which iteratively generates mathematical conjectures and attempts to prove them in Lean 4.