4 papers
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…
Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral
Sho Sonoda, Kazumi Kasaura, Yuma Mizuno +2
Understanding and certifying the generalization performance of machine learning algorithms -- i.e. obtaining theoretical estimates of the test error from the training error -- is a…
Isomorphism types of commutative algebras of rank 7 over an arbitrary algebraically closed field of characteristic not 2 or 3
Naoto Onda
We classify isomorphism types of unital commutative algebras of rank 7 over an algebraically closed field of characteristic not 2 or 3 completely.