45 citations · 97 across the 32 of their papers we have counts for
3 papers · 1 filter
Discovering New Theorems via LLMs with In-Context Proof Learning in Lean
Kazumi Kasaura, Naoto Onda, Yuta Oriike +3
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 produ…
LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving
Naoto Onda, Kazumi Kasaura, Yuta Oriike +3
We introduce LeanConjecturer, a pipeline for automatically generating university-level mathematical conjectures in Lean 4 using Large Language Models (LLMs). Our hybrid approach co…
Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs
Kaito Baba, Chaoran Liu, Shuhei Kurita +1
We present Prover Agent, a novel AI agent for automated theorem proving that integrates large language models (LLMs) with a formal proof assistant, Lean. Prover Agent coordinates a…