SnO₂WMaN.net

数理論理学

特に不完全性定理と様相論理について．

定理証明支援系

ほとんどLeanを使っています．

Webサービス開発

音MAD

数理論理学の様々な事実を定理証明支援系であるLeanを用いて形式化するプロジェクト． 私は主に様相論理を担当しています．

音MADに対して適切なメタデータを与えてデータベースを構築するプロジェクト． 設計の抜本的な見直しを考えているため，現在開発停止中です．

(Moe)₂ Chimera Maker™名義で，DJ DEKAMESHIVIVEとB2BでDJしました． 再現ミックス

Leanで形式化したSmullyanのシステムについての解説文書を書きました．

『標準的な様相論理のLeanでの形式化について』というショートトークをしました． 発表資料

第200回音MAD晒しイベントで開催される音MADエキスポの公式サイトを作成しました．

はてなブログチームにインターンとして所属し，Mastodon/Misskeyの共有ボタンの実装を行いました． 参加記録