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

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

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

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

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

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

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

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

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

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