@etale_cohomology(Etale Cohomology)2026-08-05Lean 4 とは何か ── AI が数学オリンピックに挑み、フェルマーの最終定理がコードに書き写される時代の主役言語
@etale_cohomology(Etale Cohomology)2026-08-11【連載２回目】コードなのに、そのまま数学の証明文として読める ── AIが証明を書く時代に注目すべきMizar・Isabelle・Lean 4 の宣言的スタイルの記法
@etale_cohomology(Etale Cohomology)2026-09-09【Dedukti入門 ①】Lean 4・Rocq・Isabelle が検証した証明を、もう一度、別の証明検査器で検査する ── 翻訳器と符号化ファイルの仕組み
