1976年に「コンピューターを使った数学定理の証明」が発表された際に数学者らはどう反応したのか？

2026年10月にOpenAIが社内AIを用いて得られた700点以上の「数学的成果」を発表した件は、数学者らの間で物議を醸しています。数学問題の証明にコンピューターが使われた事例は今回が初ではないとして、テクノロジー系ライターのルイス・ランスロー氏が、1976年に初めて「コンピューターによる数学定理の証明」が発表された際の数学者の反応についてまとめています。

Celebratio Mathematica — Appel — Haken and 4C
https://celebratio.org/Appel_KI/article/796/#sender

The 1st Time Machines Mogged Mathematicians
https://newsletter.pessimistsarchive.org/p/the-1st-time-machines-mogged-mathematicians

近年は最先端のAIモデルを利用して、人間の数学者が長年にわたり取り組んできた未解決問題を解決させる動きが進んでおり、OpenAIが一度に700件もの成果を公開したことは世界的な話題となりました。これに対し人間のための数学協会は、「学術的な成果を示すものではなく権力の誇示に過ぎない」と批判しています。

また、著名数学者のテレンス・タオ氏は、数学者にとって未解決問題は単に解決すればいいだけのものではなく、解決に向けた試行錯誤の過程で新しい理論や手法が生まれることも多く、その成果は最終的な答え以上に価値を持つ場合があると主張。AIが短期間で未解決問題の答えだけを生成するようになると、こうした発見の機会が失われかねないと危惧しています。そこでタオ氏はAI時代の数学研究の方向性として、AIを単に未解決問題を解く道具として使うのではなく、数学的な理解を深めたり数学知識を現実世界に役立てたりする「Math 2.0」を提唱しました。

AIが数学の未解決問題を解決しまくる現代に数学者テレンス・タオ氏が提言する「Math 2.0」とは？ - GIGAZINE

数学界がテクノロジーの発展に伴う課題を突きつけられたのは、今回が初めてではありません。1976年には「四色定理」の証明にコンピューターが用いられたことで、数学者の間でも意見が割れる事態となりました。

四色定理とは「平面上のいかなる地図も、隣接する領域が異なる色になるように塗り分けるには4色あれば十分だ」とする定理のことです。1852年にイギリスの数学者フランシス・ガスリーがイングランドの州を地図上で塗り分けていた際に気付いたとされており、その後長年にわたって数学者らが研究を進めてきました。

そして1976年、数学者のケネス・アッペルとヴォルフガング・ハーケンがコンピューターを用いた証明を発表。この証明は地図を「グラフ」という形に置き換えた上で、グラフの中にある特定の攻略可能なパターンを取り除いていくというもの。アッペルとハーケンはこの証明を行う際にコンピューターを利用し、およそ1200時間にわたる計算と100億回もの決定を実行させています。

アッペルとハーケンの発表を受けた数学者の反応はさまざまでした。ペンシルベニア大学の数学者であったハーバート・ウィルフは「神様があんなひどい方法で定理を証明させるはずがない！」と反応したほか、エディンバラ大学の数学者フランク・ボンソールは「もしその解決策が特殊なケースのコンピューターによる検証を伴うのであれば、そのような解決策は数​​学科学にはまったく属さない」として否定しました。

また、ケンブリッジ大学の数学者G・スペンサー＝ブラウンはコンピューターを使った証明は証拠にならず、数学の歴史を汚すものだと主張。アッペルとハーケンの証明は「不正行為」であると見なす数学者も存在しており、ある大学の数学科長は大学院生の意欲をそぐとしてアッペルとハーケンに会うことを禁じたそうです。

もちろん数学者の中にも、アッペルとハーケンの証明を受け入れる人々は存在しました。伝説的数学者のウィリアム・トーマス・タットは、発表以前は学術誌でコンピューターを使ったアッペルとハーケンの手法に疑義を呈していましたが、発表を受けて2人を祝福したとのこと。

また、ドイツの著名な数学者であるハインリヒ・ヘーシュも、自分自身がアッペルとハーケンが用いたアルゴリズム的手法を考案していたため証明を受け入れました。また、アッペルとハーケン以外にも同様のコンピューターを用いた証明に取り組んでいた数学者もいたそうです。

四色定理の証明作成を手伝ったハーケンの息子によると、証明を発表した際の反応は主に2つのグループに分かれたとのこと。40歳以上の人々はコンピューターによる証明が正しいものだとは納得できず、逆に40歳未満の人々は700ページにわたる手動での計算の方が信用できないと感じていたと息子は証言しています。

なお、四色定理については2026年にも日本やデンマークからなる研究チームによって新たな証明が発表され、グラフを4色で塗り分けるアルゴリズムも大幅に高速化されています。

四色定理に約30年ぶりの新証明、地図を4色で塗り分けるアルゴリズムが大幅に高速化 - GIGAZINE