202531000

計算機科学の知識も論理学の知識もない状態で定理証明支援系に入門しようとすると、いきなり「カリー・ハワード同型対応? 直観主義論理?!」となって、悩み事を相談しに行った先がヤクザの事務所だったみたいな気分になる。こっちは論理式と証明の区別すら怪しいのである。

ここを理解して Lean を使えるようになるのを今年の目標の一つにしよう。