コンピューターを使った証明

ブライアンデイビス，ロンドンキングスカレッジ
Notices of American Mathematical Society 52,No11(2005)12月
Элементыより抜粋翻訳：　https://elementy.ru/nauchno-populyarnaya_biblioteka/164681/Dokazatelstva_s_ispolzovaniem_kompyutera

コンピューター支援で証明された主要な数学的定理の最初の例は，1976年にAppelとHakenによって証明された4色の定理でした．これは2つの理由で，多くの数学者を大いに心配させました．第一に，機械が実行した計算のすべてを，手動で再チェックすることなしに証明の正しさを検証することは不可能であると主張されました．当時，「正しい」定理の証明は，ほとんどすべての数学者にとって，まだ完璧に見えました．証明の偶発的なエラーの可能性は認識されましたが，それらを修正するのは時間の問題であると考えられました．もう一つは，一部の数学者は，その定理が正しいかどうかではなく，なぜそれが正しいと見なされるのかについて考え始めたからです． 本質を理解していない証明は彼らに興味がありません．

4色定理は重要な応用がなく，長い間，面白い逸脱と見なされていました．おそらく，誇張された関心が高まったのは，この定理の単純な定式化のせいでしょう．しかし，時が経ち，コンピューターはますます利用可能になり，コンピューターの証明が広く受け入れられるようになりました．
最も新しい事例，ケプラー問題をここで取り上げます．

ケプラー問題は，最大平均密度となるように，同じ直径の球体を3次元空間に最も密に充填する方法を見つけることです．期待される解決策は昔から知られおます．1998年，トムヘイルズは，幾何学的分析と複雑なコンピュータ計算を組み合わせて，ケプラー問題に対する厳密な数学的解決策を見つけたと発表しました．ジャーナル"Annals of Mathematics"は，この論文を審査のために受け入れ，この分野の20人の主要な専門家からなる委員会を立ち上げ,専門家の委員会は，全体的な戦略を決めるためにプリンストン大学で会議を開始しました．数年が経過し，レフェリーは徐々に委員会を去りました．そして2004年の初めには，記事のレビューを続けられなくなりやめることが最終的に決定されました．ジャーナルの編集委員会は，論文の「理論的部分」を公開し，「コンピュータに基づく部分」をより適切なジャーナルに送るすることを決定しました．ジャーナルの編集委員会のメンバーであるロバート・マクファーソンは，このような論文に対するジャーナルの編集方針は破綻したことを認めた．

王立協会の会合では，コンピュータプログラムの操作の正しさを正式に証明し，それによってコンピュータを使用して証拠を調べる手順を明確にする可能性について活発な議論が行われました．マクファーソンによれば，コンピュータプログラムの正しさを証明するための実際の技術を提供できる人は学術評議会にいなかったので，問題を明確にすることはできませんでした．プログラムは，正式な数学的正しさの専門家による評価の必要性を念頭に置いて作成されたものではないので，これが大きな妨げとなりました．

証明の理論的部分に含まれるアイデアを完全に実装する完全に新しいプログラムを「ゼロから」作成することは可能です．しかし，この可能性は，専門家のレフェリーグループにとって耐え難いものとして却下されました．これは，他の科学分野のプロジェクト（土星へのカッシーニ宇宙探査機など）を完了させるために必要な労力の価値を認めている数学者はほとんどいないからです．

レフェリーの過程で，実行される計算は非常に具体的で特定の問題に特化しているため，引き出された結論を他の同様の問題に適用することはほとんどできないことが明らかになりました．

特に，ケプラーの問題は，互いにさまざまな相互作用を起こすランダムな形状とサイズの異なる物体の大規模なシステムの最小静止エネルギーを決定する問題と密接に関連しています．このような最小化の問題の例は非常に多く，個別の数値手法を開発してコンピューターで計算するので，１つづつが別物でこの分野の理解は不可能です．数学的モデリングを除いて，これらすべての問題を解決する他の方法がない場合，これらの問題のほとんどはそれほど興味深いものではありません．ただし，ケプラーの問題自体は，エラー修正コードの理論などの重要な他のいくつかの問題と関係があります．

コンピューター支援の良い面としては，コンピューターが純粋な数学者を面倒な日常的な計算から大幅に解放したことです．これは，いくつかのカテゴリに分類できます．数式処理は，絶望的に長い計算を変換することができ，さまざまな分野で広く使用されています．カオスの力学系の研究は，数値実験なしには進展しなかったでしょう．カオス現象の存在が19世紀の終わりにアンリポアンカレによって発見されたのは事実ですが，主題を理解と進歩は，コンピューターの開発を待たなければなりませんでした．自己結合行列と非自己結合行列のスペクトルの振る舞いの大きな違いは，数値実験の結果として明らかになり，現在、それ自体が厳密な数学の分野として研究されている疑似スペクトルの新しい分野を生み出しました．特に高次非線形微分方程式の分野では，コンピューター法のみが解の存在を証明することを可能にしました．