Skills
Personal History
Waseda University
Studied mathematics with a particular interest in algebraic number theory and algebraic geometry.
The University of Tokyo
Conducted research in arithmetic geometry and quasi‑homogeneous vector spaces. Earned a Master’s degree.
Interprism Inc.
Engaged in system development using Java and GitHub.
AutoRes
Involved in the development of an automated theorem‑proving system using Lean4 and Python.
Freelance
Started working as a freelancer, producing video advertisements and developing systems with Go, TypeScript, PostgreSQL and Docker.
OMRON SINIC X Corporation
Continuing to develop an automated theorem‑proving system using Lean4 and Python, as a Developer and Project Manager.
RIKEN TRIP-AGIS
Developing foundational models for automated theorem proving in the field of mathematical sciences as a visiting engineer.
Past Publications, Lectures, and Poster Sessions
Automated Theorem Proving by HyperTree Proof Search with Retrieval-Augmented Tactic Generator
SLACS2024link
Automated Theorem Proving by HyperTree Proof Search with Retrieval-Augmented Tactic Generator
AITP2024link
Automated Theorem Proving by HyperTree Proof Search with Retrieval-Augmented Tactic Generator
IBIS2024link
Automated Theorem Proving by HyperTree Proof Search with Retrieval-Augmented Tactic Generator
TPP2024link
数学推論能力を向上させる大規模言語モデルの ファインチューニングに関する研究
NLP2025link
LeanによるRademacher複雑度の形式化に向けて
PPL2025link
Lean Formalization of Generalization Error Bound by Rademacher Complexity
preprintlink