4 papers
Lean-Quantum: Toward AI-Assisted Formalization of Quantum Information
Kazumi Kasaura, Kei Tsukamoto, Kento Mori +6
Quantum information theory is built on entropic quantities; among them, the sandwiched Rényi relative entropy is a fundamental divergence with various applications, and its data p…
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…
Non-commutative linear logic fragments with sub-context-free complexity
Yusaku Nishimiya, Masaya Taniguchi
We present new descriptive complexity characterisations of classes REG (regular languages), LCFL (linear context-free languages) and CFL (context-free languages) as restrictions on…
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…