lean でのゼロ除算の扱いについて
Lean4 で選択ソートを実装します
Lean4 でフィボナッチ数列の２つの表現を実装し，同値であることを示します
Lean4 タクティクリストを公開しました
Lean日本語コミュニティができました
Lean でできたらいいなと思うこと
Lean4 + mathlib4 で圏論で出てくる図式を可視化できるよ
集合の圏での同型って弱いよねという話
Misskey を始めました。 https://misskey.io/@seasawher 数学の話はあまりしてなくて「おはよー！」とか「にゃんぷっぷー❤️」とか言ってることが多いです。たのしいよ。 Misskey ですが、 世間ではTwitter（Xと書くとわかりにくいのでこう書きます）からの避…
NNG4 全クリしました
