https://www.amazon.co.jp/dp/4627062419
Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化
発売日： 2018/4/18
>数学の高度化に伴い,従来の「紙と鉛筆」では証明の構成・検証がますます困難になるなか,
>Coqをはじめとする定理証明支援系が開発されてきました.
>こうしたシステムには,証明の正しさを保証する機能のほか,証明をコンピュータが扱える形に
>翻訳する「数学の形式化」の作業を効率化する仕組みが備えられています.
>実際Coqは「四色定理」や「ケプラー予想」といった歴史的な大問題を解くのにも利用され,
>話題をよびました.