証明とは何か

誰も読み通せない「証明」だった

1976年、アメリカのイリノイ大学から、一つのニュースが世界の数学界を駆けめぐりました。どんな地図でも、隣り合う領域を塗り分けるのに四色あれば足りる——1852年にフランシス・ガスリーがイングランドの州地図を塗り分けながら気づいて以来、124年間未解決だった「四色問題」が、ついに証明されたというのです。大学の数学科はその後しばらく、出てゆく郵便物に「FOUR COLORS SUFFICE（四色で足りる）」という誇らしげな消印を押していたほどでした。

ところが、数学者たちの反応は祝福一色ではありませんでした。ケネス・アッペルとヴォルフガング・ハーケンによるこの証明は、約1,500個の配置を計算機に1,200時間かけて検査させるもので、その計算部分を人間が読んで確かめることは事実上不可能だったからです。読み通した人が世界に一人もいない証明を、証明と呼んでいいのでしょうか。

証明は、正しさを誰でも一歩ずつ確かめられる、人類の知識のいちばん硬い足場だとされてきました。その足場の根元で、「そもそも証明とは何か」という問いが口を開いたのです。

証明とは、機械が検査できる導出である

ひとつめの見方は、証明を「公理から出発し、あらかじめ明示されたルールだけを使って結論に至る、記号の列」と定義します。源流は20世紀初頭、数学者ダフィット・ヒルベルトが進めた計画です。数学のすべてを形式的な体系の中に書き写してしまえば、証明が正しいかどうかは、書き手の権威にも読み手の直観にも頼らず、一歩一歩がルール通りかを機械的に検査するだけで決まる。曖昧さの入り込む余地はありません。

ヒルベルトの計画そのものは、1931年、ゲーデルの不完全性定理によって当初の目標を達成できないことが判明します。それでも「証明とは形式体系内の導出である」という定義は、論理学の標準として生き残りました。

弱点は、この定義が数学者の日常とかけ離れていることです。学術誌に載る証明は、自然言語と数式の混ざった「あらすじ」であって、形式的な導出そのものではありません。完全に形式化すれば長大になりすぎて、今度は人間に読めなくなる。そして機械が「正しい」と判定してくれても、なぜ正しいのかという理解は一行も増えないのです。

証明とは、共同体を納得させる社会的プロセスである

ふたつめの見方を鮮明に打ち出したのは、1979年、計算機科学者のデミロ、リプトン、パーリスの3人が発表した論文でした。定理は、証明が書き上がった瞬間に「証明済み」になるのではない。発表され、回覧され、講義で語り直され、別証明が与えられ、他の定理に応用される——そうした共同体の吟味を生き延びたものだけが、事後的に「証明された」と認められていく。つまり証明の本体は記号の列ではなく、数学者たちが納得に至る社会的プロセスのほうだ、という主張です。

数学の現場の実感をよく写した見方ですが、痛いところもあります。共同体の納得は、間違えるのです。ほかならぬ四色問題に、その実例がありました。1879年、ロンドンの法廷弁護士でもあった数学者アルフレッド・ケンプが四色問題の証明を発表し、高い評価を受けて王立協会フェローにも選ばれます。誤りが指摘されたのは11年後の1890年。パーシー・ヒーウッドが欠陥を具体例で示し、ケンプ自身も修復できないと認めました。共同体はまるまる11年、誤った証明に納得していたことになります。

導出だけでは読めず、納得だけでは信じきれない。二つの証明観の緊張がもっとも張り詰めた現場が、20世紀の終わりに現れます。

「99%確か」としか言えなかった証明

1998年8月、数学者トマス・ヘイルズは、1611年にケプラーが唱えた予想——球をもっとも密に積む方法は、果物屋のオレンジの山と同じ積み方だ——を証明したと発表しました。約300ページの論文に、大量の計算機計算。名門誌アナルズ・オブ・マセマティクスは12人の査読者による審査団を組みましたが、4年におよぶ検証の末に返ってきた報告は、前例のないものでした。証明の正しさは「99%確か」だと思うが、完全には保証できない——。論文は2005年に掲載されたものの、数学の定理に「99%」という言葉がついた事態は、関係者に重い問いを残しました。

誰よりも納得しなかったのは、ヘイルズ本人です。彼は2003年、自分の証明を、計算機で一歩残らず検査できる形式的導出に書き直す共同プロジェクト「フライスペック」を立ち上げました。証明支援系と呼ばれるソフトウェア——HOL LightとIsabelle——の上で証明の全体を組み直す作業は、10年を超えて続きます。完成が宣言されたのは2014年8月10日。人間の査読が「99%」で力尽きた証明は、こうして機械検査済みの導出に生まれ変わりました。かつての騒動の主だった四色定理も、2005年にジョルジュ・ゴンティエが証明支援系Coqの上で完全に形式化を終えています。「読めない証明」への疑念は、少なくとも検査の面では決着がついたのです。

そして2020年12月、この流れを象徴する出来事が起きます。現代数学を牽引するフィールズ賞受賞者ピーター・ショルツが、自分とダスティン・クラウゼンの新しい定理を形式化してほしいと、証明支援系Leanのコミュニティへ公開で依頼したのです。理由は率直でした。「これは私のこれまでで最も重要な定理かもしれない」。それなのに、「2019年の大半をこの証明に取り憑かれて過ごし、おかしくなりそうだった。議論を紙の上に固定することはできたが、細部まで踏み込んだ人は他にいないと思うし、小さな疑念がまだ残っている」。さらに、こう付け加えました。自分は「間違った議論でも、人をうまく説得できてしまうことが時々ある」——。第一人者の確信さえ正しさの保証にはならない、という当人による告白です。挑戦は世界中の研究者による共同作業になり、ショルツ本人が不安を抱えていた核心部分は約半年で検証を通過。2022年7月、全体の形式化が完了しました。

いま分かっていること、まだ分からないこと

見えてきたのは、二つの証明観が敵同士というより、別々の仕事を分担しているらしいことです。形式的導出が引き受けるのは「正しさの検査」です。証明支援系はこの十数年で、研究の最前線を検証できる道具にまで育ちました。一方、数学者が日々書き、読み、査読する証明は、いまもほぼすべて自然言語の「あらすじ」で、その信頼はデミロたちの言う社会的プロセスに支えられています。機械の保証が手に入っても、数学者が本当に欲しいもの——なぜ正しいのかという理解——は、人間が証明を読み、語り直すことでしか手に入らないのです。

しかも「納得」の形は、一枚岩ではなくなりつつあります。1985年、ゴールドワッサー、ミカリ、ラコフの3人が定式化したゼロ知識証明は、命題が正しいという確信だけを相手に与え、それ以外の情報を一切明かさない対話の手続きです。中身を見せずに納得だけさせる証明が数学的に可能だという事実は、「読んで理解すること」と「正しいと確信すること」が原理的に切り離せることを示しました。

分かっていないのは、切り離された後に残る「理解」の正体です。証明を理解したとき、頭の中では何が起きているのか。AIが人間の読まない証明を量産する時代が来たとき、それでも数学と呼べるものは何か。この問いはまだ開いたままです。

思い出してみてください。あなたが最近、何かを「確かめた」と言ったとき、自分で一歩ずつ辿ったでしょうか。それとも、誰かの検証を信頼したでしょうか。証明とは何かをめぐる数学者たちの論争は、知識が最後には信頼の設計の問題になるという、私たち全員の足元の話につながっています。