数学 · 22 / 25
一人では抱えきれない証明
四色定理、有限単純群、ケプラー予想。証明が成立すること、理解できること、確かめられることは、それぞれ異なる「完成」になった。
一 礼儀正しい拍手
1976年7月22日、イリノイ大学の数学者ケネス・アッペルとヴォルフガング・ハーケンが、四色で足りると発表した。通常の平面地図なら、境界の一部を共有する隣同士の領域を、必ず違う色で塗り分けられる。ただし、一点で触れるだけの領域は隣同士とは数えない。その年の8月、トロント大学で開かれたアメリカ数学会とアメリカ数学協会の夏季合同大会で、ハーケンは壇上に立ち、この証明を説明した。48歳。ベルリン生まれの位相幾何学者で、三次元空間の形を扱う分野ではすでに名が通っていた。会場は満員だった。124年間、宙に浮いていた問題に、ついに答えが出たのである。
その会場にはドナルド・アルバースもいた。彼の記録によれば、ハーケンの話が終わったとき、沸き起こるはずだと思っていた歓声は聞こえなかった。聞こえたのは、礼儀正しい拍手だった。講演後、数学者たちは次々に、どうにもすっきりしないと口にした。気になったのは、証明の姿だった。その大きな部分を機械が計算していた。計算時間は1,200時間。人間が手で、最初から最後まで確かめることはできない。何百ページもの出力のどこかに間違いが潜んでいるかもしれない、と彼らはよく言った。アルバースはそこに、間違いがあってほしいのだろうか、という問いを自分で差し挟んでいる。この報告は1981年春、ある数学雑誌に掲載された。題の前半は「礼儀正しい拍手」、後半は「今日、何を証明と呼ぶのか」だった。
問題のほうは、一度聞けば子どもにもわかる。生まれたきっかけも、ささやかなものだった。1852年、フランシス・ガスリーという若者が、イングランドの州の地図に色を塗っていた。どうやら、いつも四色で足りる。弟のフレデリックに話すと、弟は師のド・モルガンに尋ねた。10月23日、ド・モルガンはダブリンのハミルトンに手紙を書き、問いを取り次いだ。冒頭には、今日、学生からある事実の理由を説明してほしいと頼まれたが、自分はそれが事実だと知らなかったし、今もまだ知らない、という趣旨のことが書かれている。3日後の返事でハミルトンは、その色の四元数にすぐ取りかかることはなさそうだ、と答えた。四元数は、その9年前に彼自身が考え出したものだった。思いついたその日、通りかかった橋の石に式を刻みつけた。あのころのハミルトンは、すっかり四元数に取りつかれていた。
最初に問いを思いついた若者は、その年21歳で、法学の学位を取ったばかりだった。その後、この問題には戻ってこない。問題について一行も書かなかった。南アフリカへ渡り、ケープタウンの南アフリカ・カレッジで20年以上、数学の教授を務めた。数学のほかに心を注いだのは、ケープ地方のヒースだった。一人の植物学者とともに研究し、亡くなるまで続けた。彼の姓を名にいただく植物の属がある。
説明するのに1分とかからない問いを、証明するのに124年かかった。けれども、あのトロントの会場で人々がすっきりしなかった理由は、もっと前から話さなければならない。この問題は、一度、証明されていたのである。
二 11年間、生き延びた証明
問いは20年以上、引き出しの中で眠っていた。1878年6月13日、ロンドン数学会の会合で、ケイリーが、あれを解いた人はいるのかと尋ねた。翌年、かつての教え子の一人が名乗りを上げる。1879年7月、ロンドンの法廷弁護士アルフレッド・ケンプが『ネイチャー』で証明を発表し、その後、全文がアメリカの数学雑誌に載った。本業は訴訟で、数学はケンブリッジでケイリーに学んでいた。証明は明快で、着想も巧みだった。地図上で二つの色が交互につながる領域の列なら、ほかの部分に手をつけず、その列の色だけを丸ごと入れ替えられる。のちに「ケンプ鎖」と呼ばれる方法である。証明は受け入れられ、そのまま11年が過ぎた。翌1880年には、スコットランドの物理学者テイトも二つの証明を示した。そこにも鋭い着想があり、基本的な誤りもあった。この時期、多くの人が問題はもう片づいたと思っていた。
1890年、ダラムの数学講師ヒーウッドが、ケンプの証明の穴を指摘した。五つの隣接領域に囲まれた一つの領域を扱うところで、色の交換を続けて二度行う。ケンプは二つの操作が互いに干渉しないと考えた。だが、図の中では二本の鎖が絡み合うことがあり、一度目の交換が、二度目に必要な条件を壊してしまう。証明は崩れた。
ヒーウッドは、壊すだけで終わらなかった。残された方法から、少し弱い結論を証明した。五色なら、必ず足りる。鎖全体の色を入れ替える技法も生き残り、グラフ理論の常用の道具になった。失敗した証明が役に立つものを残すのは、数学史では珍しくない。ヒーウッド自身はその後、ダラムで講師から教授になり、1926年から1928年には副学長も務めた。地図の彩色にはさらに60年近く取り組み、この分野での最後の論文を1949年に発表した。87、88歳という年齢だった。同僚の記憶に残る彼は、小柄で痩せ、少し背を丸め、大きな髭を蓄えていた。変わった形の、見るからに古いマントをよく羽織っていた。授業中、教室にいることを許された犬も一匹いた。
むしろ驚くべきは、過ぎた時間のほうだ。明快に書かれた証明が、一流の数学者たちの目の前に11年間もありながら、誰も誤りに気づかなかった。人間が読めることと、誰かが実際に確かめたことは、もともと同じではない。トロントでの不安の半分は、ここから来ていた。読める証明でさえこうなのに、読めない証明は、何を根拠に信じればよいのか。
三 イリノイの計算機室
アッペルとハーケンより前に、この道で計算機を使っていた人がいる。ドイツのハインリヒ・ヘーシュだった。1960年代、彼は鍵になる方法を練り上げた。1967年にはハーケンが、この問題のために彼を訪ねている。その後の4年間、ヘーシュは何度かアメリカへ渡った。そちらのほうが計算機は大きく、速かったからだ。共同研究者の中にはハーケンもいた。ところが、いちばん大事な時期に、ドイツ研究振興協会はヘーシュへの助成を打ち切った。
1970年代の初め、ハーケンはある講演で、ブルックヘブン研究所の計算機を使った試みについて話した。計算機に詳しい専門家からは、計算で攻めても望みはないと言われたという。講演が終わると、同じ学科のアッペルがやってきた。専門家のほうが間違っている。時間はかかるが、できる。そう伝えた。二人は1972年に共同研究を始めた。計算を主に受け持つのがアッペル、理論を受け持つのがハーケンだった。
ふつうの証明を先に書き上げ、最後に機械で少し計算したのではない。機械は最初から最後まで、仕事の輪の中にいた。人が規則を決め、機械が試す。問題が見つかると人に戻し、規則を直して、また機械に渡す。何年も、その往復が続いた。最後に残った数字は、規則487本、人の目で調べた局所的な場合が約1万、機械が一つずつ検査した配置がおよそ2,000種類。遅い機械で90分かかる配置は、速い機械に移しても30分かかった。計算時間は合計で約1,200時間。二人の説明では、その間に機械はおよそ100億回の論理判断を行った。最後の段階で使えたのは、イリノイ大学が1976年3月、大学の事務処理用に購入したばかりの大型計算機だった。二人は、その稼働時間の一部を分けてもらったのである。
手仕事のほうも、二人の手だけで済んだわけではない。規則の最終版は手で導いた。1976年前半、アッペルとハーケン、そしてハーケンの娘ドロテアは、何か月もかけて、のちに一覧を構成する1,936種類の配置を一つずつ調べた。ドロテアはこのころ、中等学校から大学へ進む時期にあり、のちには自ら計算機科学の研究者になった。証明を公表する前には、両家の子どもが5人、手伝いに加わった。ドロテアとアルミン・ハーケン、ローレル、ピーター、アンドルー・アッペルである。機械の出力と照らし合わせ、論文に描いた配置に写し間違いがないか、一ページずつ確かめた。アッペルの娘ローレルは13歳。担当したのは700ページほどだった。ハーケンはのちに、ひと月を丸ごと費やして、彼女はおよそ800か所の誤りを見つけた、と振り返っている。700ページに800か所なら多くはない、そのうち650か所は彼女が自分で直し、残りは自分とアッペルがわずか5日で修正できた、という趣旨の回想だった。
一覧は、その後も姿を変えた。プレプリントでは1,936種類。正式発表時には1,482種類に減り、さらに整理されて約1,405種類になった。正式な論文は1977年に二部に分けて刊行され、検証を扱う部分にはジョン・コッホも加わった。大量の図と確認記録を収めた、約450ページ分のマイクロフィルムも付いていた。アッペルとハーケンの見積もりでは、難しい配置を一つ選び、機械の出力をすべて一人で調べようとすると、週40時間を充てても何年もかかる。十数年後の1989年、二人は証明全体を一冊の本にまとめ直した。
1976年の秋、イリノイ大学数学科は郵便料金計器に手を加えた。学科から出す手紙の一通一通に、こう押されるようになった。「四色で足りる」。
四 一つの一覧表
機械が計算していたのは、一覧に並ぶ一つひとつの項目だった。では、何の一覧で、どうしてそれが欠かせないのか。話はケンプの証明の形に戻る。1976年の証明と1879年の証明は、骨組みが同じなのである。まず、四色では足りないと仮定する。すると最小の反例があるはずだ。五色を必要とする地図のうち、領域の数がいちばん少ない地図である。そこで、二つのことを準備する。一つは局所的な配置の一覧を作り、どんな地図にも、その中のどれかが必ず現れると示すこと。これを「不可避」という。そのための方法が「放電法」だ。各領域に、隣接する領域の数に応じた数値を割り当て、規則に従って隣同士でその数値を移していく。移し終えたあと、どこかには必ず正の数が残る。その場所には、一覧にある配置のどれかが必ずできている。もう一つは、一覧の各配置が、最小反例には現れえないと示すことだ。現れたなら、その部分を縮め、もっと小さな地図にできる。小さい地図は仮定によって四色で塗れる。縮めた部分を戻しても、色をうまく入れ替えれば塗り分けられる。これを「可約」という。二つを合わせると、最小反例は一覧の配置を含まなければならず、しかも含むことができない。ゆえに最小反例そのものが存在しない。アッペルとハーケンが使った放電法は、ヘーシュから受け継いだものだった。
ケンプの一覧は短かった。彼はまず、どんな地図にも、隣接領域が五つ以下の領域が必ずあると示した。隣が四つ以下なら、色の交換で処理できる。隣が五つある場合。その一つに、ヒーウッドの見つけた穴があった。
その後の道筋は、隣が五つの場合を細かく分け、もっと大きく、もっと詳しい配置に置き換え、それぞれの可約性を個別に証明することだった。だが、細かく分けるほど一覧は長くなり、一つの配置を確かめる手間も増えていく。配置の外側には領域の輪がある。その輪に四色を並べるあらゆる場合を試し、色を入れ替えて収められるかを調べなければならない。輪が14領域なら、並べ方は20万通り近くある。18領域になると、1,600万通りを超える。
アッペルとハーケンが機械を使わざるをえなかったのは、このためだ。使ってみたかったからではない。ケンプ以来、骨組みは決まっていた。短い一覧を見つけるか、長い一覧を一項目ずつ最後まで調べるか。短いほうは、100年たっても誰も見つけていなかった。
五 三つの割り切れなさ
トロントであの日に残った割り切れなさは、のちに三つに分けられた。同じ不満を三通りに言っているのではない。
第一の立場は、これは証明ではない、というものだ。最もよく知られた議論は、哲学者トマス・ティモチコが1979年に示した。四色定理はたぶん間違っている、と言ったのではない。証明にはもともと二つの働きがある。一つは結論を信じさせること。もう一つは、論証の道筋を最初から最後まで見渡し、なぜそうなるかをつかませること。彼が後者に与えた名は、「全体を見渡せること」を意味した。一人の人間が一か所に立ち、すべてに目を通せるということだ。1976年の証明は前者を果たし、後者を失った。見渡すことのできない計算まで証明と認めるなら、その時点で「証明」という語の意味は広がったことになる。
第二の立場は、証明ではあるが、美しくない、というものだ。なぜ、ほかでもない四色で足りるのか。その理由を教えてくれない。トロントの会場にいた多くの人は、いつか、短くて、そうなるわけのわかる証明が現れることを願っていた。
第三は、いちばん実際的な不安である。証明なのかもしれないが、本当に間違いがないか確かめられない。プログラムに欠陥はないか。一覧に抜けはないか。数千件の出力のうち、どれかを誤って処理していないか。印刷されたデータが受け渡しの途中でずれていないか。同じ1979年、デミロ、リプトン、パーリスの三人は、証明の信頼性は形式的な推論だけから生まれるのではない、と論じた。数学界に持ち込まれ、批判され、簡単にされ、別の場所で使われ、教えられていく。その過程全体が、証明を確かなものにする。誰にも全体を検算できない証明では、その過程をどこから始めればよいのか。
その後の進展が本当の意味で答えたのは、第三の不安だけだった。1990年代、ロバートソン、サンダース、シーモア、トマスの四人は、初めはアッペルとハーケンの証明を確かめようとした。だが、すぐに断念する。のちに彼らが書いたところでは、一部は計算機に依存していて手では調べられず、手で調べられるという部分も、驚くほど複雑で細部が多かった。千種類以上の配置の記述を、一つずつ入力するだけでも大仕事になる。そこで、自分たちでやり直した。1996年に完成した証明では、配置の一覧は633種類、放電規則は何百本から32本に減った。プログラムとデータも公開され、ほかの人が自分で実行し直せるようになった。彼らの説明では、不可避性を示す部分は、手で確かめると数か月、計算機なら20分ほどだった。機械は取り除かれていない。しかし、機械が受け持つ部分は初めて、別の人が独立に検査できる対象になった。2005年にはゴンティエが、この新しい証明全体を「証明支援系」と呼ばれるプログラム上の形式体系に書き込み、ごく小さな中核プログラムに、一段ずつ検査させた。検査したのは1996年の道筋であって、1976年にアッペルとハーケンが実行したプログラムではない。あのプログラムに欠陥がなかったかどうかは、今もこの方法では証明されていない。以後、信頼を置く先は、何千何万もの場合と長大な専用プログラムではなく、小さな中核、形式的な定義、そして元の命題を形式言語へ移すその一歩になった。信頼は消えたのではない。範囲が小さくなり、置き場所がはっきりし、人を替えて確かめられるようになった。
第二の割り切れなさは、解消されていない。2026年3月、6人の著者がプレプリントで、新しい証明と、はるかに速い彩色法を提案した。使う可約配置は、二つの簡単な場合を含めて8,202種類である。2026年10月1日現在、これは著者たちが提案した新証明と呼ぶべきもので、長期にわたる独立の検証を経て、広く確定した結論として扱うべきものではない。慎重であることは、誤りだと判定することでもない。参加者の一人、トマッセンは、計算機を使わない証明が欲しい、そのことを考えるのをやめたことはない、と語っている。
六 一冊に収まらない定理
二つ目の例は、もっと大きい。一冊の本に収まりきらないほどに。
前の回で、一つの骨組みを見た。二つを合成でき、何もしないものが一つあり、一つひとつを打ち消せる。数学者はこれを群と呼ぶ。正規部分群と、それに対応する商群を使って群を分解していくとき、自明でも全体そのものでもない正規部分群を持たない群を、単純群という。自明でない部分群を一切持たない、という意味ではない。その位置づけは、素数に少し似ている。整数は素数を掛け合わせてでき、どの有限群にも、単純群を因子とする組成列がある。ただし、因子がわかっただけでは、元の群がどう組み立てられていたかは一つに決まらない。では、有限の単純群には、いったいどんなものがあるのか。
いちばん小さい単純群は素朴である。素数個の元が輪をなす。正五角形を一回転の5分の1ずつ回すと、5回で元の位置に戻る。この五通りの回転が、一つの単純群になる。順序を入れ替えられない単純群の最初の例は、元を60個持つ。正二十面体の回転をすべて集めたものだ。第10回で見た、五次方程式には一般的な解の公式がないという話も、根までたどっていくと、この60個の元を持つ単純群に行き当たる。
答えは、一つの名簿になった。一定の規則に従ってどこまでも続く、いくつかの無限の系列。それに、どの系列にも属さない26個の孤立した例外が加わる。その最大の例外は、のちに「モンスター」と呼ばれた。元の個数を書き下すと54桁になる。1973年前後、フィッシャーとグリースがその存在を予言した。1980年1月14日、グリースはアナーバーで構成の成功を発表した。19万6,883次元の対象の対称性をすべて集める、という作り方だった。1982年の発表論文で、彼はそれを「親しみやすい巨人」と呼んだ。
まず、一編ごとの論文が長くなっていた。1963年、ファイトとトンプソンは、位数が奇数の有限群はすべて可解群であると証明した。したがって、非可換な有限単純群の位数は必ず偶数になる。論文は255ページに及び、数学雑誌の一号を丸ごと占めた。のちにゴンティエ率いるチームが、この論文をそっくり証明支援系に移し、2013年に発表した。
その名簿に漏れがない、と示すのが有限単純群の分類定理である。一編の論文でも、一冊の本でもない。数百編の論文に、中心となった著者がおよそ100人。本文だけで約1万ページあり、必要な背景の結果まで含めると、1万5,000ページという見積もりもよく使われる。数え方は統一されていない。そもそも、この証明がどこまで続くのか、境目をはっきり引けないからだ。
1980年代初め、ダニエル・ゴレンシュタインは、『有限単純群――分類への入門』という趣旨の題を持つ本を出版した。20年以上にわたる仕事を、すでに完成した一つの全体としてまとめたのである。その20年以上、彼は全体を見渡し、進む方向を定め続けてきた。のちに、最も深く関わった一人であるアッシュバッハーは当時を振り返り、分類は1980年前後には完成していた、というのが数学界の一般的な認識だったと書いている。
ここでいう完成は、ある日、誰かが壇上で口にした一言ではない。研究計画が、徐々に公認の成果へと変わっていく過程だった。大きな枝はすべて処理できたと考えられ、残る部分についても、その分野の専門家ならどうすればよいかを知っている。それが根拠になっていた。
専門家が完成させ方を知っていることと、公刊され、一つひとつを引用できる完全な証明が揃っていることは、同じではない。その二つの文の隙間に、問題が隠れていた。
七 欠けていた部分
分類の中には、「準薄群」と呼ばれる大きな一群がある。第一世代の計画で、この部分を受け持ったのはジェフ・メイソンだった。1980年に分類を発表し、1981年には約800ページの手稿を残した。しかし出版はされず、のちになって、それが未完成で、重大な欠落を含むことが明らかになった。
この欠落には、発見された日がない。1890年のヒーウッドのように、ケンプのある一手を指して、ここが間違いだと言ったのではなかった。少しずつ、輪郭が見えてきたのである。1980年代末から1990年代、分類の証明を整理し直すにつれ、この部分を決着済みの一段として扱うことが、次第にできなくなった。とうに終わったと思われていた仕事が、実は終わっていなかった。
穴を埋めたのは、アッシュバッハーとスティーヴン・スミスだった。2004年、二人は全二巻の『準薄群の分類』を出版する。合わせておよそ1,220ページ。一枚の正誤表を添えたのではない。まるごと新しい本を書いたのだ。その後も小さな抜けがいくつか見つかったが、それらも一つずつ埋められた。
だから、ここで確かに言えることは三つある。名簿は1980年代初めには、正しいものとして数学界に受け入れられていた。第一世代の公開された証明文献には、実際に、大きな未完成の部分があった。そして2004年の二巻が、その部分に、完成した、出版できる形の証明を与えた。
ゴレンシュタインは早くからわかっていた。第一世代の証明は、たとえ正しくても、最終形として満足のいく姿ではない。リチャード・ライアンズ、ロナルド・ソロモンとともに、第二世代の計画を始めた。数百編に散らばった証明を、体系的で、できるだけそれだけで読め、依存関係の明らかな一組の専門書に書き直す。1992年8月、ゴレンシュタインは亡くなった。第二世代の第1巻が出たのは、1994年になってからだった。出版社の説明も、目標を、細部まで慎重に述べた、おおむね自己完結した証明としている。第10巻は2023年に刊行された。書き直しはその後も続いており、巻数や総ページ数は出版の進行に合わせて更新しなければならない。ライアンズとソロモンは主要な道筋の最後の部分を書いている。ドイツのシュトロートも、その締めくくりを担う大部の手稿を抱えている。当初の見積もりだった全12巻、5,000ページでは、今やずいぶん窮屈そうだ。
第一世代の証明を、それが依拠する結果まで含め、初めから終わりまで一行ずつ読んだ人はいるのだろうか。そうしたと言う人は、一人も見つからない。アッシュバッハー、ライアンズ、ソロモンらは、全体の構造を並外れた深さでつかんでいる。各分野には、それぞれの専門家がいる。けれども、構造を把握することと、数百編の論文を一ページずつ照合することでは、仕事の桁が違う。
数学界が実際に採った方法は、超人的な読者を一人探すことではなかった。それぞれの分野の専門家が、自分の持ち場に責任を持つ。論文同士で結果が繰り返し使われ、そのたびに見直す機会が生まれる。ただし、引用されるたびに誰かが全行を調べ直す、という保証はない。大きな欠落が見つかれば、書き直す。そして概説や第二世代の専門書を通して、誰が誰を信じているかという関係を、どの結果がどの結果に依存するかという関係へ、できるかぎり置き換えていく。ある定理が知られていることは、その細部をすべて知る人が一人いることを意味しない。
八 三つの完成
三つ目の例がある。1611年、ケプラーは六角形の雪の結晶について小さな本を書き、支援者への新年の贈り物にした。その中で、あることをついでに予想した。果物屋のオレンジを、何段もピラミッド状に積むあの積み方が、すでに空間に最も密に球を詰め込む積み方なのではないか。問いの発端は砲弾だった。ウォルター・ローリーが助手のハリオットに、積み上げた砲弾の個数を数える方法を考えさせたのである。ハリオットは1606年からケプラーと文通していた。1900年、ヒルベルトはこの問いを、あの問題集の第18問題に含めた。1998年、トマス・ヘールズが証明を発表する。半分は従来どおりの推論、半分は大量の不等式の確認、線形計画法、そして有限個の場合の列挙だった。重要な部分では、学生のサミュエル・ファーガソンが大きな役割を果たした。
『アナールズ・オブ・マセマティクス』は、この論文のために12人ほどの査読チームを組み、約4年をかけた。2003年、チームの責任者フェイエシュ・トートは、証明が正しいという確信は99パーセントあるが、計算の全部を認証することはできない、と述べた。この数字は、のちに数えきれないほど引用された。査読について、ふだんは口にされない事実を数字にしたからだ。査読は、正しいか間違いか、二つの位置しかないスイッチではない。2005年、同誌は主要な論証を掲載した。1,065ページから1,185ページまで、計121ページ。計算用の資料や、関連する計算の論文は、別に提供または発表された。
ヘールズは、そこで足を止めなかった。証明の全体を形式体系に書き込み、機械の小さな中核に検査させる計画を立ち上げた。あの計算を信じてほしい、と査読者に頼まなくて済むようにするためである。2014年8月10日、計画の完了が発表された。使われた証明支援系は二つ。2017年、この形式化された証明は、22人の名を連ねて正式に出版された。
同じ定理に、三つの日付、三つの意味での完成がある。1998年、著者はできたと考えた。2005年、雑誌は、掲載するに足る信頼性があると判断した。2014年、形式的な検証の中核が、検査を終えた。
この問いに、このシリーズで出会うのは四度目になる。第3回では、あの本を公理化の始まりと呼んでよいのかと問うた。第5回では、あの注釈は証明なのか。第9回では、あの級数は微積分なのか。前の三度は、あるものを何と呼ぶべきかという問いだった。しかも、後世の人が振り返って問うていた。今度は違う。ものは目の前にあり、名前にも争いはない。問われているのは、それが「知られた」と言えるのかどうかだ。そして今回は、同時代の人が問うている。1976年、トロントの会場を出るころには、数学者たちはもう、どうにも落ち着かないと言っていた。3年後、ティモチコはその落ち着かなさを、一つの問いとして書いた。
別の側からの声も、絶えずあった。1980年、クラコフスキーはティモチコに応じ、有限の長さの形式的証明なら、原理的にはどれも見渡せる、人類はもう少し長生きすることを覚えればよい、と述べた。皮肉だが、その中には堅い芯がある。数学はこれまで、一つの証明の背景を全部、同時に一人の頭へ収めることなど要求してこなかった。20ページの論文が、数千ページの本にある定理を使うことはある。それで、その20ページを証明ではないと言う人はいない。1994年、サーストンは、数学者が探しているのは、人が数学を理解し、考えられるようにする方法だ、と書いた。そう考えるなら、証明は結論の正しさを保証するだけでなく、何かを人の手に渡さなければならない。巨大な証明の問題は、すべてを持っている人がいないことではない。ふだんの数学でも、誰もすべては持っていない。困るのは、信頼の鎖が長くなることだ。よい方法は、その輪を一つひとつ、できるだけ小さくし、できるだけ別の人にも確かめられるようにすることである。
だから、1976年から今日までの本当の変化は、数学が人の手から機械へ渡ったことではない。もともと一つに結ばれていた三つのことが、初めて大きな規模で分かれたのである。論証は成立しているか。人に理解をもたらしたか。そして、実際に確かめられるか。四色定理では、計算が一人の視野の外へ出ていった。分類定理では、文献と専門知識が一人の視野の外へ出ていった。形式化は、それらをもう一度、機械が一歩ずつ点検できる対象へと収めようとする。何を根拠に信じてよいのか。その問いのかなりの部分には答えている。けれども、もう一方は残る。数学界が、あることは真だと確かに知っているなら、それは、なぜ真なのかも理解しているということなのだろうか。
一人では抱えきれないものも、分ければ、一つひとつは誰かの手に収まる。
1977年、マサチューセッツ工科大学の三人の若者が、一つの暗号方式を公開した。頼りにしたのは、数学のある難しさだった。大きな素数を二つ掛けるのは簡単だが、その積から元の二つを取り出すのは難しい。5年後、この方式には会社ができ、6年後には特許がついた。
数を計算する営みは続いていく。けれども、何を数学に数えるのかは、まだ一度も決着がついていない。
史料と関連文献
以下の資料は、本文の歴史的な細部や解釈の分かれる点に対応している。所蔵記録、古代の文学作品、現代の復元は、同じ性質の証拠ではない。