Euler's Eyes
2026-10-26
機械のための記法：コンピュータが確かめる証明
二千年のあいだ、数学の証明は人が読むために書かれた文章だった。「明らかな」段階を飛ばしたり、図にたよったり、共同体の約束を使ったりできた。残りは読み手が補ったのである。この五十年で、何ひとつ補わない読み手が現れた。コンピュータである。
四つの色
となりあう国がちがう色になるように地図を塗るには、何色あれば足りるか。答えの四色は 1852 年に予想され、一世紀以上も抵抗した。1976 年、イリノイ大学のケネス・アッペルとヴォルフガング・ハーケンは、問題を二千近くの場合に帰着させ、それをコンピュータに一つずつ、千時間以上の計算時間をかけて確かめさせることで証明した。
学界は割れた。人間がだれも全部を読めない証明は、証明なのだろうか。支持する人々は、長い証明の多くもまた、だれにも全部は読まれていないことを指摘した。批判する人々は、プログラムには誤りがありうると言った。2005 年、フランスのジョルジュ・ゴンティエは、コンピュータの部分も含めて証明全体を、Coq という証明支援系で書いた。それは公理から出発して論理の一歩一歩を確かめるものである。疑いは場所を移した。「プログラムは正しいか」ではなく、「確かめる側は正しいか」になったのである。それはずっと小さく、点検しやすいプログラムである。
ケプラー予想
1611 年、ケプラーは、オレンジをもっとも密に積む方法は八百屋のピラミッドだと主張した。1998 年、アメリカのトーマス・ヘイルズは、数百ページの議論と大がかりなコンピュータ計算を組み合わせた証明を発表した。査読者のチームは四年間取り組み、正しさを「99% 確信している」と述べた。ヘイルズは残りの 1% に満足せず、証明全体を形式言語で書く Flyspeck 計画を始めた。2014 年、何十人もの協力者とともに計画は完了した。機械が一歩一歩を確かめたのである。
Lean
今日、数学者にもっともよく使われている証明支援系は Lean で、2013 年に、当時マイクロソフト・リサーチにいたブラジルのレオナルド・デ・モウラが作った。そのまわりに mathlib が育った。何百人もが書いた、数十万の形式化された定理をもつ共同のライブラリである。2020 年、ドイツのフィールズ賞受賞者ペーター・ショルツェは、自分でもすべての細部を確かめたか自信のない自分の結果を形式化するよう、共同体に呼びかけた。「液体テンソル実験」（Liquid Tensor Experiment）は 2022 年に終わった。結果は正しく、形式化によって証明を簡単にできる箇所も見つかった。
Lean の一行は次のようなものである。
theorem soma_comuta (a b : ℕ) : a + b = b + a := Nat.add_comm a b
「任意の自然数 $a$、$b$ について $a + b = b + a$ であり、証明はライブラリの交換法則の定理である。」何ひとつ言わずにすませていない。各文字の型も、各段階の出どころも。これは第7章の線形の書き方を極限まで推し進めたものであり、第4章のことばによる証明を、機械が確かめられる文法に翻訳したものである。
練習：三色では足りないとき
中央の国が三つの国に囲まれ、その三つの国はそれぞれほかの二つと国境を接している。この地図には四色が必要であることを示せ。
四つの国は二つずつ国境を接している。中央の国は三つすべてに接し、三つの国もたがいに接している。だから各国はほかのすべての国とちがう色を必要とし、四色が必要になる。定理が保証しているのは、地図がどれほど複雑でも、五色が必要になることは決してないということである。
練習：Lean の一行を読む
theorem soma_comuta (a b : ℕ) : a + b = b + a := Nat.add_comm a b という行で、仮定、主張、証明を見分けよ。
(a b : ℕ) は文字を宣言している。$a$ と $b$ は自然数であり、文章でいう「$a$、$b$ を自然数とする」にあたる。コロンのあとが主張 $a + b = b + a$ である。:= のあとが証明で、ここではライブラリですでに証明された定理を参照しているだけである。第 5 の文章で見た Algol の := が、新しい意味でまた現れている。「…と定義される」あるいは「…によって証明される」である。