数学者も証明を間違える

【 数学者も証明を間違える 】

では、なぜ、数学者はコンピュータを使い始めたのでしょうか？  それには、理由があるように思います。

第一の理由は、人間の手にはあまるが、コンピュータなら解ける巨大なサイズの問題が存在するからです。一般的な解法は見当たらなくても、場合の数が有限なら、すべての場合をしらみつぶしに総当たりでチェックができるなら、問題を解くことができます。

数学の証明問題へコンピュータが最初に使われたのが、こうした方法が使われた「四色問題」であったことは象徴的です。このことは、コンピュータを使って、そういうタイプの問題に、人間がチャレンジすることが可能になったのだとも言えます。前回見たヘイルズの「ケプラー予想」の証明も、こうしたタイプの証明でした。

ただ、場合の数が有限だとしても、シラミつぶし総当たりの方法が、実際にコンピュータで実行可能とは限りません。このタイプの問題は、たくさん存在するのですが、実際にコンピュータで解けるのは、場合の数が小さい時だけです。

さらに、難しい数学の問題がすべてこのタイプである訳ではありません。むしろ、数学者の多くが取り組んでいる問題は、こうしたタイプの問題ではないのです。ですから、数学者が証明にコンピュータを使い始めたのには、別の理由があります。

第二の理由は、証明が複雑になると、証明が正しいことが検証しにくくなるからです。先に、証明が長すぎて、「その証明を、全部読んでいる数学者は誰もいない。」というブラック・ジョークを紹介しました。先に紹介した「Feit–Thompson定理」の証明は、このケースです。

　「そうだ。コンピュータを使った巨大な証明なんか信用できない。誰がその正しさを保証するんだ。」　

確かにその通りです。ただご安心を。現代の巨大証明は、検証ずみの証明支援システムを利用して、それ自身の正しさを検証しながら、証明を実行します。その意味では、1970年代にアッペルとハーケンが行った「四色問題」の証明と、21世紀になってからのゴンティエによる「四色問題」の形式的証明とは、本当は異なるものです。

証明の長さだけが、問題ではありません。例えば、全く新しいアイデアに基づく証明は、その正しさを（彼が数学の専門家であったとしても）第三者に確信させるのは難しいのです。

ペレルマンは、2002年から2003年にかけて arXiv に投稿した論文で、「三次元のポアンカレ予想」を解きました。ただ、その証明が「正しい証明」と公式に認められたのは、2006年になってからでした。彼は、業績を認めないアカデミーの対応（認めないというより、理解できなかったのだと思いますが）に腹を立て、数学をやめフィールズ賞の賞金の受け取りも拒否しました。

　「大丈夫。わしの証明は、エレガントで、誰が見ても正しいことがわかる。」

本当でしょうか？

数学者が証明にコンピュータを利用し始めている、第三の理由は、次のような事実に基づいています。

　「数学者は、証明で間違いを犯すことがある。」
　「しかも、本人は、それに気づかない。」

【 「証明へのコンピュータの利用-- その背景と変化の意味を考える」を公開しました 】

https://youtu.be/0k8oQ2QtkoE?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg

スライドのpdfは、次からアクセスできます。https://drive.google.com/file/d/1bYuddwlGnd1nqAUhm1Xks8T8HStLlTaL/view?usp=sharing

このトピックのまとめページは、こちらです。ほぼ毎日更新されると思います。 https://www.marulabo.net/docs/math-proof/

セミナーへのお申し込みは、こちらからお願いします。
https://math-proof.peatix.com/