Hello! I'm Asei Inoue (井上亜星 in Japanese).

I studied mathematics at Kyoto University and earned my Master's degree on Mathematics at RIMS (Research Institute for Mathematical Sciences Kyoto University).

I am currently learning about Lean language. The Lean language would bridge pure mathematics and computer science, creating a new mathematical community. My ambition is to make Lean, after TeX, the programming language known to all mathematics graduates.

To this goal I was involved in setting up a community called lean-ja. My main interest at present is to enrich Lean's Japanese documentation.

• 1997.09: be born into this world
• 2016.04-2020.03: Kyoto University, Bachelor of Science
• 2020.04-2022.03: Kyoto University, Master of Science (Mathematics)
• 2022.04-2024.01: web engineer.
• 2024.02-now: software engineer at Proxima Technology

• 「Lean でのドキュメント・教科書作成ツール」 / 第27回プログラミングおよびプログラミング言語ワークショップ（PPL 2025）
• Lean言語は新世代の純粋関数型言語になれるか？ / 関数型まつり2025
• Leanで本を執筆する / TPP2025
  • これはPPL2025での発表と本質的に同じ内容
• Lean プロジェクトの依存関係を 自動更新する / λ Kansai in Winter 2026

• An Additive Approximation Scheme for the Nash Social Welfare Maximization with Identical Additive Valuations
• n月刊ラムダノート Vol.5, No.1(2025)/自然数を作って学ぶLean言語
• 「ゼロから始めるLean言語入門 ― 手を動かして学ぶ形式数学ライブラリ開発」ラムダノート

• Please use Discord for private discussions. seasawher is me.

Thank you for your support!

• github-readme-stats