Coq/SSReflect/MathCompによる定理証明 フリーソフトではじめる数学の形式化/萩原学/アフェルト・レナルド

萩原学アフェルト・レナルド
森北出版
ISBN：4627062419/9784627062412
発売日:2018年04月

---

【内容紹介】
コンピュータと協働して数学する!
定理証明支援系Coq/SSReflect/MathComp、待望の入門書.

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

◆日本語初のチュートリアル
本書は、Coqとその拡張言語SSReflect/MathCompの初となる解説書です.定理証明支援系の研究利用と普及を手がけてきた著者らが、開発環境のインストール手順から基本的な操作、代表的な命令・ライブラリの使い方までを案内します.集合論、代数学、確率・統計、そして情報理論の簡単な定理を題材に、Coq/SSReflect/MathCompの使い方を易しく例示.本書をひととおり読みこなせば、幅広い分野の定理を形式化する力が自然と身につくはずです.

◆まずは触ってみよう!
数学者を目指す方は「大規模証明時代の必須ツール」として、プログラマの方であれば「ソフトウェア検証などの応用を見据えた基礎トレーニング」として、Coq/SSReflect/MathCompに触れてみてはいかがでしょうか.コンピュータと手を携えて定理をつくっていく――その新感覚の面白さに、きっと魅了されることでしょう.