前回の記事で私はこんなことを書きました． Lean で数値計算ができるようになればもっと多くの層が取り込めることが期待できるのですが，現状では難しそうです． seasawher.hatenablog.com 改めて考えてみると，数値計算は丸め誤差と打ち切り誤差がどうして…

Lean を学び始めて8カ月がたちました．

数学科の就職と Lean 言語について私が今思っていることを書きます．

大学受験のときの自分の行動を振り返って，良かったことと悪かったことを考えます．

中学校に，ひどい先生がいたという回想．

今回は，最近見つけて使い始めたブラウザ拡張機能の宣伝をします． LeechBlock です． 私は自制心が皆無で，いちどTwitterやTogetterを見始めるとやめることができなくなってしまいます．気づいたら夜中の３時になっていて，翌朝の仕事に差し支える事態にな…

転職先が決まったので体験談をメモします

定理証明支援系 Advent Calendar 2023 参加記事．初心者向けに，Lean Prover のおもしろさ，魅力を解説します．

予防接種を受けた日記

線形代数の無料で閲覧できる学習リソースを少し調べました

静的サイトジェネレータ (SSG) についていろいろと調査をしたときのメモを公開します．

型理論のリソースを探したのでメモします．

lean でのゼロ除算の扱いについて

Lean4 で選択ソートを実装します

Lean4 でフィボナッチ数列の２つの表現を実装し，同値であることを示します

Lean4 タクティクリストを公開しました

Lean日本語コミュニティができました

Lean でできたらいいなと思うこと

Lean4 + mathlib4 で圏論で出てくる図式を可視化できるよ

集合の圏での同型って弱いよねという話

Misskey を始めました。 https://misskey.io/@seasawher 数学の話はあまりしてなくて「おはよー！」とか「にゃんぷっぷー❤️」とか言ってることが多いです。たのしいよ。 Misskey ですが、 世間ではTwitter（Xと書くとわかりにくいのでこう書きます）からの避…

NNG4 全クリしました

Lean4 の勉強をしています

自分が中学生だった頃，クラスに『数学ガール』を読んで数学が好きになったという人がいたんですよ．*1 その人とはたまに数学の話をしたりしてました． 高校が違った *2 ので高校以降は会ってなかったんですが，一度だけ電車で乗り合わせたことがあります．*…

圏論について

集合についてのくだらない疑問

LeetCodeの布教記事です

CS50Web修了しました

数学は論理の学問だと思わないで欲しいという話．

何かの技術・学問を学びたい社会人へのアドバイス．実はプログラミングの話が大半です．