定理証明支援の紹介 - Qiita目的 定理証明支援とは何かと現状の整理。 定理証明支援とは 定理証明支援とは数学の定理を自動で証明することではなく、ステップバイステップでコンピュータに命令を送り、数学の定理を証明するのを助けるシステムである。 支援だから意味ないということでなく、最近の数学の証明は長くなり証明の検証が難しいのを助ける意味がある。定理証明支援の意義についてはこちらが詳しい。 また、信頼性が求めらる難しいアルゴリズムの検証、たとえばTLS(暗号通信)やRaft(分散合意アルゴリズム)のサーバーに利用されつつある。 ここでいう定理は大げさなものだけでなく、$1+1=2$、$0*何か=0$、$a*b=b*a$といった簡単なものを証明しながらどんどん積み上げていく。通常のプログラムと違うのは証明であるので使用する変数が整数ならそのすべての値について成り立つ定理を証明する。 定理を証明するのに使うツールは下記である。
