二千年のあいだ、数学の証明は人が読むために書かれた文章だった。「明らかな」段階を飛ばしたり、図にたよったり、共同体の約束を使ったりできた。残りは読み手が補ったのである。この五十年で、何ひとつ補わない読み手が現れた。コンピュータである。 四つの色 となりあう国がちがう色になるように地図を塗るには、何色あれば足りるか。答えの四色は 1852 年に予想され、一世紀以上も抵抗した。1976 年、イリノイ大学のケネス・アッペルとヴォルフガング・ハーケンは、問題を二千近くの場合に帰着させ、それをコンピュータに一つずつ、千時間以上の計算時間をかけて確かめさせることで証明した。 四色で塗られた地図。となりあう二つの地域が同じ色になることはない。Inductiveload · ウィキメディア・コモンズ · CC BY-SA 3.0 学界は割れた。人間がだれも全部を読めない証明は、証明なのだろうか。支持する人々は、長い証明の多くもまた、だれにも全部は読まれていないことを指摘した。批判する人々は、プログラムには誤りがありうると言った。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章のことばによる証明を、機械が確かめられる文法に翻訳したものである。 共同体を変える記法 形式化は仕事のしかたを変えつつある。2024 年にイギリスのケヴィン・バザードが始めたフェルマーの最終定理の形式化のような計画には、会ったこともない何十人もの協力者が集まり、それぞれがひとつの補題を形式化する。継ぎ目は機械が確かめるので、部品はきっと組み合わさるという確信がある。記法はまたしても、だれがどのように参加できるかを決めている。