泡のカフェオレ
コンピュータを使って数学を少しでも楽にやれる手段として、、定理証明支援系（定理の証明を支援してくれるソフトウェア）を使って、定理の証明を確実に行なったり、部分的に証明を自動化することが挙げられます。
このブログで紹介している数式処理システムによる計算の支援、とはまた異なる方向での数学へのコンピュータの応用と言えます。
この記事では定理証明支援系 Lean による定理証明支援をゲーム感覚で知ることのできるサイトNatural Number Gameを紹介します。まだこのサイトで出来ることを全部終了していないのですが、ここまでに知ったことの備忘録も兼ねての記事です。
定理証明支援系 Lean、、、多分初めて聞くかたも多いのではないでしょうか。公式サイトはこちらになります。2013年にMicrosoft Research（マイクロソフトの研究所）で開発が始まり今日まで開発が続いています。Leonardo de Mouraという方が始めたようです。この証明支援系の開発とともに、数学者のコミュニティによるmathlibの開発も進んでいます。Mathlibは数学の様々な分野をLeanの書式で形式化して、それらの分野の定理の、Leanを使った証明が蓄積されたものです。解析、幾何学、数論、トポロジー、圏論など幅広い数学が取り扱われています。
Natural Number Gameは、Leanの使い方を、勉強するためのサイトです。ロンドンのインペリアルカレッジの先生が作成しているようです。素材として自然数を取り上げています。ペアノの公理から初めて、自然数の様々な性質を証明していきます。とは言ってもペアノの公理を扱うためには、等号、命題論理なども必要です。それらを用いて加法、乗法、冪乗などを定義して、その性質をLeanの力を借りて証明していきます。
ゲーム、と言っても呪文、フォース、HPなどは登場しません。が、全体が10個の世界から構成されています。これらを順に全てクリアすると、Leanの初歩的な使い方を習得できるようになっています。最初から順に、チュートリアル世界, 加法世界、乗法世界、と進み、命題論理の世界、進んだ命題論理の世界、進んだ加法の世界、を通過し、進んだ乗法世界の後、最後の不等式の世界に至ります。定理を積み上げ、新しい定義を導入しながら、それなりに複雑な定理を証明して終わります。
各世界の中にはいくつかのレベルが設定されており、各レベルには１つの定理がゴールとして、定理の仮定とともに提示されています。その提示されたゴールを仮定を使って証明することが目標です。１つ世界には４つから１０個くらいのレベルが設定されています。例えば一番最初のチュートリアル世界では４つのレベルがあります。
各レベルの定理の証明は人間が行うことです。最初は定理そのものがゴールとして設定されています。人間が簡単な指示をコマンドを使って行うと、Leanがそのコマンドに基づいてゴールを変形します。この指示を適切に繰り返し、ゴールを自明な形に変形することが出来れば証明は完了します。例えばゴールが等式で両辺が全く同じになった、とか、ゴールと同じものが仮定に含まれている、という状態になれば、証明を完了させることが出来ます。
Leanが証明完了を表示した場合、それまでに指示したコマンドの列が正しい証明であることがLeanによって保証されます。「証明間違い」はありません！
チュートリアルの一番最初の例題を見てみましょう。
左側のlemma example1には「補題：x, y, zがmynatである時、x*y+z=x*y+z。」とあります。これが証明したい定理です。
右の65:0: error:という部分にはx, y, z: mynatを仮定として、x*y+z=x*y+zを証明することがゴール、と表示されています。これが現在のゴールです。まだ指示を与えていないので、定理とゴールが一致しています。
各レベルのページには、新しく学ぶ概念やコマンドの説明があります。このページでは（上図では省略しましたが）「ゴールが等式で等号の右辺と左辺が全く等しい場合、refl, と打ち込むと、証明を完成させることができる」とあります。そこで、
Proof: begin 64の右側の入力フィールドをクリックし、refl, (カンマまで)を打ち込むと画面にProof Completeと表示され、証明が完了します。これでレベル1をクリアしました！！
等号では反射律(x = x)が成り立つので、反射律(reflection)を適用せよ、と指示したわけです。その結果証明は完了しました。
チュートリアル世界では、もう１つ重要な指示を勉強します。rwというコマンドです。仮定の中にある等式をゴールに適用してゴールを変形することを指示します。
上図では省略していますが、最初にゴールとしてsucc(succ(a))=succ(b)が表示されています。
Proofの中に見える91 の右の rw h, という指示で、ゴールに仮定h:succ a = bを適用します。この結果ゴールが、succ (b) = succ (b)と変化します。等号の左右が全く同じになったので、relf, コマンドで証明を完了します。
今まで指示とかコマンド、と呼んでいたものは正式にはtactic（戦略）と呼ばれています。推論規則のようなものですが、高度なtacticは自動証明につながる道具になります。他のtacticも紹介します。
apply h 仮定hが\(A\rightarrow B\)の形の時に、ゴールが\(B\)であれば、ゴールが\(A\)になります。仮定を利用してゴールを十分条件に書き換えます。
exact h 仮定hとゴールが同じ場合に、証明を完了します。
split ゴールが\(A \land B\)の形の場合、ゴールを２つのゴール\(A\)と\(B\)に分けて両方とも証明の必要なゴールとします。
right/left ゴールが\(A \lor B\)の形の場合、rightであれば\(B\)を、leftであれば\(A\)を新しいゴールとします。どちらか一方が証明できれば良いわけです。
ここまでのtacticを使うことで等号を含んだ命題論理はかなり証明できるようになります（矛盾を導くexfalsoというtacticはちょっと複雑なので省略します）。
自然数の加算、乗算はペアノの公理に加えて、演算の定義が与えられます。公理、既知の定理、演算の定義、上述のtacticを使って簡単な定理は証明できますが、複雑な定理には数学的帰納法のtacticであるinductionを使う必要があります。変数を指定してinduction を使うと、ゴールが２つになります。１つはその変数が0の場合、もう１つは変数がnの時に成り立つことを新たな仮定として加えて、変数がsucc(n)の場合の２つのゴールです。 これらの２つのゴールを証明すれば、全体の証明が完了します。
やってみるとわかるのですが、tacticの選択を間違えれば、エラーが発生したり、先に進まなかったりします。inductionを入れ子で使えばゴールの管理も必要です。こういったことはすべてLeanが管理してくれるので、人間は試行錯誤でtacticを選び、ゴールに向かって突き進めば良いのです、、、ゲーム感覚ですね。
今回はLeanとNatural Number Gameサイトの概要をご紹介しました。次回は形式的証明の実際を少しだけ見てみます。
