定理証明リンク集

定理証明、特に定理証明支援系(Proof Assistant)はその存在こそ少しずつ浸透しつつあるような気がしないでもないけれど資料とか全然まとまってないのが不便だなと前々から思っていたのでリソースをまとめておきます。

これも追加してほしいみたいなのあったら教えてください。

Proof Assistants

始めるなら次の中から選ぶのがよいと思います。

  • Coq
    • Calculus of constructionsベースの型システムとリッチなコマンドを備えた言語
    • このリストの中では最もコミュニティが大きい、入門書等も豊富
    • 型システムと項を書くためのGallina, コンパイラへの命令を記述するためのVernacular, タクティクスの定義に使うLtacなどの言語が混ざって出てくるのが初心者には混乱必至
    • 結構複雑な言語なので使いこなすのはそれなりに大変
  • Agda
    • Martin-Löf type theoryベースの言語
    • Coqと違ってコマンド等はとても貧弱だが言語が薄いので中の仕組みが分かりやすい、依存型の勉強にはもってこい
    • 実践的に使おうとするとパフォーマンスが悪いのがネック モジュール分割や証明のスキップみたいな面白くないところに時間を取られる可能性あり
  • Idris
    • Agdaに似た感じの言語
    • この中では唯一純粋なプログラミング言語として使用可能(runtimeがあって実行可能コードを吐ける)だが実際に動かして使うにはまだまだという感じ
    • Agdaよりはサポートが多く証明が書きやすいはず(未検証なので嘘かも)
  • Lean
    • この中では後発、CoqやAgdaに似ており、Agdaよりは書きやすくリッチでCoqよりは薄くて簡単
    • 数年前にメジャーバージョンが2から3に上がりそこで多少の断絶があるらしい
    • 機能網羅的なリファレンスがまだ用意されてないらしいのでCoqやAgdaの知識がないと使いこなすのは難しいかもしれない
  • Isabelle
    • この中では唯一Curry-Howardをベースとしない形式証明(依存型もない)
    • 豊富なライブラリと強力なproverによる自動証明が魅力
    • 「普通の」数学をやりたいならこれがおすすめ
    • 公式のリファレンスはあるが機能は膨大、非公式ドキュメントも少ないので習得は骨が折れるかも

入門書等

出版されていてもドラフト版のpdfが無料で読めるものが多い

入門記事等

読み物もあり

私が書いてる記事とか

それなりに色々書いたつもりではあるので まぁ参考になればくらいの気持ちで(話半分で読んだ方がいいやつとかもある)

その他リソース