定理証明支援系についての問題意識 | 雑記帳定理証明支援系 (proof assistant / interactive theorem prover) というのは、専用の言語で書いた証明を機械にチェックさせるツール、およびその証明の記述を支援するツールです。Rocq（旧名Coq）、Agda、Lean、Isabelleなどが有名です。 この記事では、定理証明支援系について私が感じている問題意識を説明します。私自身は定理証明支援系のヘビーユーザーではないので、もっと勉強したり、定理証明支援系を使い込んだりすれば答えが見つかるのかもしれません。詳しい方からのフィードバックを頂けると嬉しいです。 このブログでは、過去に定理証明のできる依存型プログラミング言語Idrisを使った定理証明を扱いました。10年以上前ですが……。 Idrisで遊んでみた (0) (2014-02-27) Idrisで遊んでみた (1) (2014-02-27) I
「型の理論」と証明支援システム -- COQの世界
