2 papers
cs.AI2025
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…
math.AC2021
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.