aesop タクティクで手軽に自動証明をします

Lean 関連活動振り返り

zenn に投稿を始めました

11月になったので振り返り

いままであまり書いていなかったような気がするのですが、「個人ではなくコミュニティが成長する」というのは Lean の大きなメリットだなと思います。 どういうことかというと、「人間が手動で証明を検証する」いわゆる普通の数学と、Lean などの定理証明支…

数学をやり直したい

Lean 関連活動の振り返り

Lean 関連の活動の 4-7 月の振り返り

日記

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

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

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

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

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

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

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

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

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

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

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

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

NNG4 全クリしました

Lean4 の勉強をしています