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.

I am looking for people and companies to sponsor my OSS!

• 2016.04-2020.03: Kyoto University, Bachelor of Science
• 2020.04-2022.03: Kyoto University, Master of Science (Mathematics)
• 2022.04-2024.01: a job in the software industry(1st company)
• 2024.02-now: a job in the software industry(2nd company)

• 「Lean でのドキュメント・教科書作成ツール」 / 第27回プログラミングおよびプログラミング言語ワークショップ（PPL 2025）

• An Additive Approximation Scheme for the Nash Social Welfare Maximization with Identical Additive Valuations
  • arXiv
  • accepted to the Journal of the Operations Research Society of Japan (JORSJ)
• n月刊ラムダノート Vol.5, No.1(2025)/自然数を作って学ぶLean言語

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

• github-readme-stats