定理証明支援系とは、数学の定理証明を支援するソフトウェアのこと。数学者のツールとして、そしてソフトウェア開発のツールとして、近年注目を集めています。

直近では、「Proof Summit 2019」というイベントも開催されます。募集を開始して早々に席が埋まってしまったとのことで、関心の高さがわかります。https://proof-summit.connpass.com/event/141191/

2018年4月に発行された、『Coq/SSReflect/MathCompによる定理証明』（萩原学、アフェルト・レナルド著）は、定理証明支援系の代表格であるCoqとその拡張言語SSReflect/MathCompの初となる解説書です。以下に、同書の第1章から抜粋します。「定理証明支援系って何？」「何ができるの？」ということに興味がある方は、ぜひご一読ください。

＊＊＊

Coq/SSReflect/MathCompとは（1.1節　はじめに）

著：萩原学、アフェルト・レナルド

本書はCoq/SSReflect（＊1）/MathCompによる数学の形式化の入門書です。想定している読者は「数学の証明をしっかり身につけたい人」、「大学1年生程度の数学（集合論、代数学など）を学んだことのある人」など、数学と証明に興味のある方々です。Coq、SSReflect、MathCompに関する予備知識は必要ありません。むしろ、それらの言葉を聞いたことのなかった読者を歓迎します。本書を通じてCoq/SSReflect/MathCompの基本的な使い方を習得すれば、数学の証明を厳密に書く力が向上するでしょう。あくまで数学の形式化を目的としているため、Coq/SSReflect/MathComp自体の原理は深く解説しません。本節ではCoq/SSReflect/MathCompとは何か、それらを使って何ができるか、はたまたどんなことができそうか、といったことを例を挙げながら述べていきます。

＊1　Ssreflectと表記することもあります。本書では名前の由来であるSmall Scale Reflectionを意識してSSReflectという表記を採用しています。

■定理証明支援系と形式化
SSReflectとは、証明言語とよばれるコンピュータ（計算機）上の言語です。数学の定理・補題・言明（＊2）・証明を記述できます。SSReflectで書かれた定理・補題・言明・証明の正しさをチェック（検証）するソフトウェアがCoqです。そのようなソフトウェアは定理証明支援器とか定理証明支援系とよばれます。定理証明支援系は検証だけでなく、定理証明を支援する便利な機能をもちます。たとえば、定理証明支援系を利用して証明したことのある補題を一覧表示・検索する機能、証明の途中で残っているサブゴールを明示する機能などです。図1.1に、Coqによる証明検証中のサブゴールの遷移イメージを書きました。左のサブゴールに対してタクティクとよばれる命令（ここではmove=>A B C.のこと）を伝えると、右のサブゴールへと遷移する様子を表しています。

図1.1　「move=> A B C」によるゴールエリアの遷移

＊2　本書における命題、定理、補題、言明の意味をまとめておきます。命題とは論理的に真か偽のどちらか一方が定まる主張のことです。とくに、真であるものを定理、補題とよびます。言明とは、命題の主張を表す文章や記号の列です。数学書では、命題を「定理と補題」のような意味で用いる場合がありますが、本書ではそうでないことに注意してください。

SSReflectによる三段論法の証明を例示します。表1.1をご覧ください。言明とその証明を「私たち人間の日常の言葉（ここでは日本語）」と「証明言語SSReflect」のそれぞれで記述しました。左右それぞれが対応しています。

表1.1　SSReflectによる三段論法の証明

SSReflectの証明を初めて見た方は、何が書いてあるのかさっぱりわからないかもしれません。ところが、慣れてくると、左側に書かれた日常言語による証明との対応が読み取れるようになります。

このように、人間の日常言語と証明言語は文法も単語も異なります。そこで数学の教科書に書かれた定義や証明を、定理証明支援系向けに変換する作業が発生します。その作業を形式化とよびます。

形式化は現代の数学や計算機科学に大きなインパクトを与えています。その一つの理由として、「人間には正しいかどうかチェックするのが難しい定理の証明であっても、定理証明支援系を用いれば検証できる」ことが挙げられます。

証明のチェックが難しい定理の代表例として四色定理が挙げられます。いかなる地図も隣接する領域の色が異なるよう色を塗るには、4種類の色があれば十分という定理です。1852年に予想されましたが、証明されたのは1976年でした。この証明の一部には、複雑な場合分けを計算機で行う手順が含まれていました。複雑さに加えて計算機を使うことの珍しさから、証明の検証が必要だと考えられました。そこで、ゴンティエ（＊3）は定理証明支援系Coqを用いて四色定理の形式化を2000年に開始し、2004年に完成させました。そのようにして四色定理は正しいことが検証されたのですが、実のところ、SSReflectは四色定理の形式化を簡便にするツールとして開発された言語なのです。

＊3　ジョルジュ・ゴンティエ（Georges Gonthier, 1962～）：カナダのコンピュータサイエンティスト。

もう一つ、チェックの難しい証明の例を挙げます。群論のファイト‐トンプソンの定理（奇数位数定理）の証明です。これは、書籍に換算すると数百ページに及ぶ長大な証明です。証明の長さに加え、高度な専門知識、数十ページにわたる背理法を用いるなどの理由から、プロの数学者でも証明すべての検証は困難と言われています。しかし、2012年9月、ゴンティエ率いるフランスの国立情報学自動制御研究所（INRIA）とフランスのマイクロソフトリサーチの合同研究チームがこの定理の証明を形式化し、Coq/SSReflectで完全にチェックしました。すべての証明を記述するまでにかかった労力は、15人がかりで7年と言われています。ちなみに、MathCompライブラリはファイト-トンプソンの定理を形式化する際に必要となった補題の形式化をまとめたものです。

現在でも、形式化の研究は世界中で盛んに行われています。CoqやSSReflectなどのツールの開発だけでなく、その基礎となる数学の研究も注目されています。とくに注目されているのがホモトピー型理論です。数学で最も権威があることで知られるフィールズ賞を受賞したボエボドスキー（＊4）が考案したもので、トポロジーと形式化を結びつける理論です。この研究が発展すれば、将来的には複雑な証明を簡便に記述できるようになると期待されています。

＊4　ウラジーミル・ボエボドスキー（Vladimir Voevodsky, 1966～2017）：ロシアの数学者。

Coq、SSReflectは世界の科学界から高い評価を受けています。Coqは世界最大の計算科学系の学会であるACM (Association for Computing Machinery)から、2013年にACMソフトウェアシステム賞とACM SIGPLANプログラミング言語ソフトウェア賞を受賞しています。SSReflectを開発したゴンティエは、2011年にEADS基金グランドプライズを受賞しています（＊5）。

＊5　EADSは会社名で、現在のエアバス・グループ社です。

定理証明支援系を利用し、正しさを保証したい動機を二つ挙げます。

大規模で複雑な定理の検証：
数学の証明は、ときに、非常に規模が大きくなったり、複雑になったりすることがあります。人間が正しさを保証することが困難なほどの規模です。

四色定理やファイト‐トンプソンの定理のほかにも、こんな実例があります。1611年、ケプラー（＊6）はある予想を立てました。「無限の空間において同半径の球を敷き詰めたとき、最密な充填方法は面心立方格子である」というものです。この言明はヒルベルトの第18問題として選定され、ケプラー予想とよばれていました。ケプラー予想は長らく未解決だったものの、米国のトーマス・ヘイルズ（＊7）によって1998年に解決されました。ヘイルズはその証明を数学の有名な学術雑誌に投稿しました。しかし、複数の査読者が4年以上かけて証明のチェックを試みましたが、正しさを保証できませんでした。証明が大変長く、複雑だったからです。結果的に、その論文は2005年に出版されましたが、証明の完全なチェックはなされないままでした。それを受け、ヘイルズはFlyspeckプロジェクト（Formal Proof of Kepler Conjectureプロジェクト）とよばれる形式化のプロジェクトを開始しました。彼の証明を定理証明支援系でチェックするプロジェクトです。2003年に始まったこのプロジェクトは2014年に完成しました。一つの定理を形式化するのに、12年もの歳月がかかったのです。はたして定理証明支援系の力を借りて証明の正しさが完全にチェックされ、400年の問題に幕が下ろされました。

＊6　ヨハネス・ケプラー（Johannes Kepler, 1571～1630）：ドイツの天文学者。
＊7　トーマス・ヘイルズ（Thomas Hales, 1958～）：アメリカの数学者。

安全なソフトウェアの開発：
私たちの社会を支えているIT（情報技術）システムの安全性は日を追うごとに重要となっています。ソフトウェアにバグが潜んでいた場合、たとえそのバグが小さなものであっても、それを悪用したサイバー攻撃が行われて甚大な被害につながる恐れがあります。ですから、バグを防ぐ開発方法が望まれます。もし、ソフトウェアが正しい動作しかしないことを証明できれば、バグがないことをはじめから保証できることになります。実はこういうことにも、定理証明支援系を利用できます。実際、C言語コンパイラCompCert、オペレーティングシステムseL4は、定理証明支援系を利用して開発されてきました。これらのソフトウェアは高く信頼されています。

■定理証明支援系のもたらす可能性
ここまで、Coq/SSReflect/MathCompをとりまく現状を述べました。では、将来的にどんなことが起こるでしょうか。期待を含めていくつかの予想を述べていきます。

大規模証明時代の必須ツール：
数学の定理の多くは、論文や本などに証明が書かれています。それは、そうした定理の証明のサイズがそれほど大きくないことを意味します。しかし、先述のように定理によっては大規模な証明が必要なときもあります。たとえば、有限単純群の分類定理の証明は紙面で数千ページを超えると言われています。また、四色定理の証明は数百パターンの場合分けが必要とされています。現在、そのような定理はごく僅かです。しかし将来的に、そのような定理が数多く登場すると考えるのは不自然ではありません。大規模な証明のチェックは人間には時間的に不可能です。そうしたとき、定理証明支援系が役立つと考えられます。今後、定理証明支援系や形式化が普及すれば、そのような定理の出現が加速するかもしれません。さらに、大規模な証明を複雑に組み合わせた、超大規模な証明が生まれるかもしれません。もしそうなれば、もはや人間には証明の検証が望めなくなり、定理証明支援系による検証を基盤とした科学分野が誕生すると予想できます。

個人が検証した定理の公開（ビッグマスデータ構想）：
インターネット上に、形式化された理論が公開されていくと予想できます。現在は、数学者や数学の愛好家が、形式化されていない様々な理論をホームページ上に記述しています。しかし、それらの理論が論理的に正しいかどうかは必ずしも保証されていません。定理証明支援系が普及すれば、個人が正しさをチェックしてから理論を公開できるようになります。公開する側も観覧する側も、どちらも互いにチェックできるので信頼性の高い情報を発信・受信できるようになります。将来的には、数学の正しい理論のデータ化が進むことで、ビッグマスデータが誕生すると予想できます。そうなれば、ビッグマスデータにデータ解析技術を適用することで、関係ないと思われていた理論間に意外な共通点が見つかるかもしれません。つまり、科学の新しい手法につながると期待できます。証明の解析技術を応用することで、定理の自動証明が可能になるかもしれません。

ICTとしての論理力習得のための自己学習システム：
数学の問題を論理的に正しく証明するのは非常に難しいことです。自分では正しいと思っていても、意外なところで論理の飛躍が残ることは珍しくありません。定理証明支援系に証明をチェックさせることで、自分の考えた証明が正しいかどうか確認できます。定理証明支援系に正しさを保証してもらえるような証明を考えていくことで、論理的思考の自己学習が可能となるかもしれません。どうでしょう。わくわくしませんか。

以上でCoq/SSReflect、形式化についてのおおまかな解説を終わりにします。次節では、理論や技術に踏み込んで解説していきます。すぐに使いたい、とりあえず試してみたい、という方は1.3節「インストール・設定・環境」に従ってインストールを行い、第2章へ進んでも大丈夫です。Coq/SSReflectの仕組みに興味が湧いたら、適宜、本章へ戻るとよいでしょう。

出典：『Coq/SSReflect/MathCompによる定理証明』第1章

萩原　学（はぎわら・まなぶ）
1974年、栃木県足利市生まれ。栃木県立足利高校、千葉大学理学部数学科を経て、2002年、東京大学大学院理学研究科博士課程修了。博士（数理科学）。東京大学生産技術研究所（2002年～）を経て、独立行政法人産業技術総合研究所（2005年～）の在職時に、中央大学研究開発機構にて機構准教授（2008/4～2014/3）、ハワイ大学にてResearch Scholar（2011/3～2012/2）などを兼任。2013 年より千葉大学准教授。現在に至る。専門は符号理論とそれにかかわる離散数学、組合せ論など。趣味は映画・ドラマの鑑賞、旅行、新しい技術を体験することなど。著書に『符号理論』、『進化する符号理論』（いずれも日本評論社）。

アフェルト・レナルド（Reynald Affeldt）
1976年、パ=ド=カレー県ランス市（フランス）生まれ。2000年、ナンシー国立高等鉱業学校Ingénieur Civil des Mines課程修了。2004年、東京大学大学院情報理工学系研究科博士課程修了。博士（情報理工）。東京大学大学院情報理工学系研究科研究員を経て、2005年より国立研究開発法人産業技術総合研究所、主任研究員。

＊＊＊
『Coq/SSReflect/MathCompによる定理証明：フリーソフトではじめる数学の形式化』

コンピュータと協働して数学する！
定理証明支援系Coq/SSReflect/MathComp、待望の入門書。

【目次】
第1章　Coq/SSReflect/MathCompとは
第2章　使ってみよう
第3章　命令
第4章　MathCompライブラリの基本ファイル
第5章　集合の形式化
第6章　代数学の形式化
第7章　確率論と情報理論の形式化