45 citations · 97 across the 32 of their papers we have counts for
32 papers
Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols
Masato Kamba, Hirotake Murakami, Akiyoshi Sannai
Code-driven auditing fails when correctness depends on what the specification requires rather than how the code is written. Production blockchain networks expose this directly: byz…
Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization
Banri Yanahama, Akiyoshi Sannai
AI-driven autoformalization of mathematics is advancing rapidly. However, the type checker of a proof assistant guarantees only the logical correctness of proofs; it does not verif…
SPECA: Specification-to-Checklist Agentic Auditing for Multi-Implementation Systems -- A Case Study on Ethereum Clients
Masato Kamba, Akiyoshi Sannai
Multi-implementation systems are increasingly audited against natural-language specifications. Differential testing scales well when implementations disagree, but it provides littl…
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…