定理証明支援系とは、数学の定理証明を支援するソフトウェアのこと。数学者のツールとして、そしてソフトウェア開発のツールとして、近年注目を集めています。 直近では、「Proof Summit 2019」というイベントも開催されます。募集を開始して早々に席が埋まってしまったとのことで、関心の高さがわかります。https://proof-summit.connpass.com/event/141191/ 2018年4月に発行された、『Coq/SSReflect/MathCompによる定理証明』（萩原学、アフェルト・レナルド著）は、定理証明支援系の代表格であるCoqとその拡張言語SSReflect/MathCompの初となる解説書です。以下に、同書の第1章から抜粋します。「定理証明支援系って何？」「何ができるの？」ということに興味がある方は、ぜひご一読ください。 ＊＊＊ Coq/SSReflect/