定理証明支援系

定理証明支援系(theorem proof assistant)

数学の定義や定理、証明を記述するための形式的言語

ユーザーと対話的に証明を作成するための環境

定理証明(thorem proving)

形式化

数学の教科書に書かれた定義や証明を、定理証明支援系向けに変換する作業

定理の証明の各ステップで、どの推論規則や公理が使われたかを例外なく全て記録すること

数学の証明の正しさを担保するのはとても難しい。Kepler予想の証明の査読をしていたが手作業では結局完了できなかったため定理証明支援系(Isabelle/HOL)の力で証明した。

現代数学は難しくなりすぎて計算機の力を借りないと厳しい

定理証明支援系の言語

確認用

Q. 定理証明支援系とは

Q. なぜ計算機上で数学の証明をするか

参考