ソフィスト，ゴルジウスの第三定理
Дмитрий Германович Фон-Дер-Флаасс，«Квант» №5, 2010
3番目の定理-何かがわかっている場合、それは隣人には説明できません。
これらは現代数学で最も燃えている問題であり、おそらく最も巨大な問題です。何かを証明しましたが、その証明を他の人に伝えることはできません。あるいは、本当にそれを証明したことを他の人に納得させることはできません。この範疇で最初の例であり最も有名なのは、4色問題です。しかし、これはまだここで発生する最も困難な状況ではありません。4色問題について少しお話しした後、さらに異常な状況を示します。
図： 5.
4色問題とは、グラフ理論の問題です。グラフは、エッジで接続されたいくつかの頂点から成ります。これらの頂点を平面上に描画し、エッジが互いに交差しないようにエッジを接続できる場合、平面グラフと呼ばれます。グラフの頂点に異なる色を塗り，エッジを挟んで隣接する頂点は異なる色になるように塗分ければ正しい塗分けと呼ばれます。できるだけ少ない色でグラフを正しく塗り分けたい。図5には、3つの頂点（互いにエッジで結ばれている）が，1つの頂点にエッジで結ばれているところがあります。つまり、このグラフを描くには4色必要です（十分なことは？）。
百年もの間、未解決の問題でした：平面上に描くことができるどんなグラフも4色で着色できるというのは本当か？誰かは信じて4色で十分であることを証明しようとし、また別の誰かは信じずに4色では反例を考え出そうとしました。問題は非常にわかりやすい定式化がされているので、多くの人々、アマチュア数学者まで、それに挑戦し証明しようとしました。そして、彼らは膨大な量の怪しげな証拠、または、怪しげな反例を提示しました。彼らはそれらを数学者に送り新聞で叫んだ。私は4色問題を証明しました！
誤った証拠を書いた本まで出版されました。要するにノイズばかりでした。
結局、K。AppelとV.Hakenがそれを証明しました。ここで、証明のスキームについて説明します。同時に、この証拠が他の人には説明できない理由もわかります。人々は、平面グラフがどのように組み立てられているかの地道な研究から始めました。彼らは数十の構成のリストを提示し、平面グラフなら、これらの構成の1つが必ず見出だせることを証明しました。これは証明の前半です。そして、証明の後半-これらの構成のそれぞれについて、グラフがその構成を満たすか調べれば、4色で塗分けできることを確認できます。
証明は背理法で行い、グラフが4色で着色できないと仮定します。前半のリストから、4色で塗分けできる平面グラフの満たすべき構成はわかっています。それらの構成のそれぞれについて、次のような推論が実行されます。グラフにこの構成が含まれていると仮定します。そのグラフは捨てましょう。残ったものは4色に塗られています。そして、残りの部分をどのように4色に塗っても、この構成で塗れることを確認します。
カスタマイズ可能な構成の最も単純な例は、3つの頂点だけに接続されている頂点です。グラフにそのような頂点があるならば、最後まで塗りっぱなしにしておけばいいことは明らかです。他は全部塗って、この頂点が何色につながっているかを見て、4つ目を選びましょう。他の構成については、推論は似ていますが、より複雑です。
さて、これはどのようにして行われたのでしょうか？これだけ多くの構成の一つ一つを手で確認するのは無理がありますね～時間がかかりすぎます。そして、このチェックはパソコンに割り当てられていました。そして、多くのケースにあたり、本当にそうであることを確認しました。その結果、4色問題が証明されました。
推理の人間がやった部分は、分厚い本に書かれていて、すべてが塗られた最終チェックをコンピューターに託したという文が添えられていて、コンピュータープログラムも与えられていました。このプログラムでは、すべて計算して、すべてをチェックしています - 本当に、すべてが大丈夫なので、4色問題の定理が証明されています。
すぐに騒動が起こりました-そのような証拠は信じられません。結局のところ、証拠のほとんどは人間ではなくコンピューターで生成されたものです。 「コンピュータが間違っていたらどうしますか？」 -偏狭な人たちが言いました。
そして、この証明に問題は実際ありましたが、それらはコンピューターの部分ではなく、人間の部分にあることが判明しました。証拠に欠陥が見つかりました。もちろん、複雑な検索を含むこのような長さのテキストにはエラーが含まれている可能性があることは明らかです。これらのエラーは見つかりましたが、幸いなことに修正されました。
ヨハネスケプラー
コンピュータによる部分は残り、それ以来、同じ種類の検索を行うだけで、プログラムの書き直しだけで、複数のコンピュータでチェックされました。結局のところ、正確に何を列挙すべきかが言われれば、誰もが独自のプログラムを作成して、結果が期待どおりになることを確認できます。たとえば、証明にこのような大規模なコンピュータ列挙を使用することは問題ではないように思われます。どうしてでしょう？しかし、同じ理由で、4色問題の例ですでに明らかになっています。つまり、人間の証拠よりもコンピューターの証拠の方がはるかに信頼されています。彼らはコンピューターが機械だと叫びました。機械は突然どこかで故障し、消失が起きます。コンピュータが誤ってどこかで誤動作し、エラーが発生した場合（0が誤って1に置き換えられた場合）、これによって誤った結果が生じることはありません。これは結果につながりません。それはプログラムが最終的に壊れることだけです。コンピューターが実行する典型的な操作は何でしょうか？レジスターからそのような番号を取得し、そこに制御を移しました。当然、この数に1ビットの変更が発生した場合、制御はどこにも移されませんでした。そこにいくつかのコマンドが書き込まれ、すぐにすべてが破壊されます。
もちろん、コンピューター用のプログラムを書く際にエラーが発生する可能性がありますが、これはすでに人為的なエラーです。人はプログラムを読んで、それが正しいかどうかを確認することができます。人は他人の証明を読んで、それが正しいかどうかを確認することもできます。しかし、人間はコンピューターよりも間違っている可能性がはるかに高い。他の人の十分な長さの証明を読んで、それに間違いがある場合、あなたがそれに気付かない可能性があります。どうしてか？まず第一に、証明の作者自身がこの間違いを犯したので、それはそれが心理的に正当化されることを意味します。つまり、彼は偶然にそれをしたのです-これは原則として、典型的な人がそのような間違いを犯すことができる場所です。これは、この一節を読んで、それに気づかないことで同じ間違いを犯す可能性があることを意味します。したがって、人間による証明の人間による検証は、コンピュータプログラムの結果を他のマシンで再度実行して検証するよりも、信頼性の低い検証方法です。 第二に，ほぼすべてが正常であることを保証していて、第一は幸運だった時です。
そして、この問題（人々が書いた数学のテキストの誤りを見つけること）では、それはますます困難になり、時には不可能にさえなります-これは現代の数学の深刻な問題です。あなたはそれと戦わなければなりません。まだ誰も知らないが、問題は大きく、現在発生しています。いくつかの例があります。これはあまり知られていませんが、最も近代的な例の1つ、ケプラー予想です。それは、３次元空間にボールを詰める方法です。
図： 6
まず、2次元空間、つまり平面で何が起こるかを見てみましょう。同じ円を作りましょう。それらが重ならないように平面上にそれらを描くための最良の方法は何ですか？答えがあり-あなたは六角形の格子のノードに円の中心を置く必要があります。
3Dでは、どのようにボールをしっかりと詰めますか？まず、図6に示すように、平面上にボールを配置します。次に、図7に示すように、同じ層の別の層を上に置きます。次に、同じ層の別の層を上に置きます。直感的には、これは3次元空間にボールを置くための最密な方法です。ケプラーは、この詰め方は3次元空間で最密充填でなければならないと主張しました。
17世紀に始まったこの予想は、注目され続けて、21世紀の初めに、その証明が現れました。誰もがそれを手に入れて読めるインターネット上のパブリックドメインにあります。この記事は200ページです。それはある人によって書かれ、コンピュータ計算だけでなく、純粋に数学的な推論も含まれています。
図： 7
まず、著者は数学的な推論を使用して、有限数のケースをチェックするように、問題を減らします。その後、時々コンピューターを使用して、彼はこの有限の、しかし非常に多くのケースをチェックし、すべてが落着します。万歳！ -ケプラーの予想が証明されました。そして、これが問題の記事： 誰もそれを読むことができません。重いので、場所によっては検索が本当に完了したかどうかが完全には明確でなく、それを読むのは単に退屈だからです。 200ページの退屈な計算。人はそれを読むことができません。
一般的に言って、誰もがこの記事にはこの定理の証拠が含まれていると信じています。しかし一方で、これまで正直にチェックした人は誰もいません。特に、この記事は査読ありのジャーナルに掲載されていません。自尊心のある数学者は、「すべて正しい。ケプラー予想が証明された」とサインすることができません。
そして、これは唯一の状況ではなく、これは数学の他の分野でも起こります。最近では、集合理論、モデル理論、さまざまな分野で未解決の問題のリストに出くわします。ある仮説に対するコメントがあり、このような記事で反駁されていると言われていますが、誰もそれを信じてはいません。
これが状況です。その命題を証明しましたが、それを他の人に伝えることができません。
最も恐ろしい例は、有限単純群の分類です。ここで、それが何であるか、群とは何か、有限群とは何かには深入りしません。有限群はすべて、ある意味で、単純群［訳注）自明な正規部分群以外に正規部分群のない群．従って，小さなブロックに分解できないという表現もなりたつ］と呼ばれる単純なブロックから組み立てられています。これは、小さなブロックに分解することはできません。これらの有限単純群は無限にあります。それらの完全なリストは次のようになります。これらは17のエンドレスシリーズであり、最後に26の個別群［訳注）散在型単純群］が追加されますが、これらは個別の方法で構築され、どのシリーズにも含まれていません。このリストには、すべての有限単純群が含まれていると言われています。この仕事は数学にとって必要なことです。したがって、70年代に、その解決策に対するいくつかの特別なアイデアと希望が現れたとき、さまざまな国、さまざまな機関の数百人の数学者が問題を攻撃し、それぞれが独自の作品を取り上げました。いわば、このプロジェクトのアーキテクトがいて、これらすべてをまとめて1つの証明にまとめる方法を大まかに想像していました。人々が急いで競争していたことは明らかです。その結果、彼らが行った作品は合計で約10,000の雑誌ページになり、それが出版されたものです。また、プレプリントまたはタイプされたコピーのいずれかの形式で存在した記事もあります。私自身、そのような記事を読みました。この完全な証拠の注目すべき部分が含まれていますが、公開されることはありませんでした。そして、これらの10,000ページは、さまざまな人によって書かれ、さまざまなジャーナルに散在しており、さまざまな程度の理解力があります。これに関係がなく、この理論の設計者ではない一般の数学者にとって、10,000ページすべてを読むことは不可能であるだけでなく、非常に困難です。証拠の構造そのものを理解します。そしてそれ以来、これらの作者の何人かは死にました。
証明は誰も読めないテキストの形でしか存在しないが、分類が完了したことが発表され、次のトラブルにつながった。新しい数学者は、有限群の理論に行く気がありませんでした。これを行う人はますます少なくなっています。そして、50年後には、この証拠で何かを理解できる人が地球上にまったくいないということが起こるかもしれません。伝説があります：私たちの偉大な祖先は、すべての有限単純群がリストされており、他にはないことを証明する方法を知っていましたが、今ではこの知識は失われています。かなり現実的な状況。しかし、幸いなことに、この状況が現実的だと思っているのは私だけではないので、彼らはそれに苦労しており、彼らは特別なプロジェクト「有限単純群の分類の証明に関連する哲学的および数学的問題」を組織したとさえ聞いた。この証拠を読みやすい形にしようとしている人々がいます、そして多分いつかそれは本当にうまくいくでしょう。これらすべての困難をどうするかを考えようとしている人々がいます。人類はこの仕事を覚えているので、最終的にはそれに対処します。しかし、それにもかかわらず、他の同様に複雑な定理が現れる可能性があり、それは証明できますが、誰も読むことができず、誰にも言うことができないという証拠です。