2026-09-03T21:00:00+09:00

「証明できない」ということを証明する — Löbの定理をLeanで100行

「自分の正しさは自分では保証できない」という話を、どこまで機械に証明させられるか。Lean 4で約100行、公理依存なし。定理・前提・政策の境界線と、第2不完全性定理の親戚たちを図とスイッチで辿る読み物。