四色定理のコンピューター証明を巡る数学界の分断

およそ1200時間じかんの計算けいさんと100億回おくかいもの決定けっていをコンピューターに実行じっこうさせて示しめされた「四色定理よんしょくていり」の証明しょうめいは、1976年ねんの発表当時はっぴょうとうじ、数学界すうがくかいの意見いけんを大おおきく割わる事態じたいとなりました。「平面上へいめんじょうのいかなる地図ちずも、隣接りんせつする領域りょういきが異ことなる色いろになるように塗ぬり分わけるには4色しょくあれば十分じゅうぶんだ」とするこの定理ていりは、1852年ねんにイギリスの数学者すうがくしゃフランシス・ガスリーが気きづいて以来いらい、長年ながねんにわたって研究けんきゅうされてきた難問なんもんでした。

証明しょうめいを発表はっぴょうしたケネス・アッペルとヴォルフガング・ハーケンは、地図ちずを「グラフ」という形かたちに置おき換かえた上うえで、特定とくていの攻略可能こうりゃくかのうなパターンを取とり除のぞいていく手法しゅほうをとりました。しかし、その検証けんしょうをコンピューターに委ゆだねたことに対たいし、一部いちぶの数学者すうがくしゃからは激はげしい反発はんぱつが起おこりました。ペンシルベニア大学だいがくのハーバート・ウィルフが「神様かみさまがあんなひどい方法ほうほうで定理ていりを証明しょうめいさせるはずがない！」と反応はんのうしたほか、エディンバラ大学だいがくのフランク・ボンソールは「もしその解決策かいけつさくが特殊とくしゅなケースのコンピューターによる検証けんしょうを伴ともなうのであれば、そのような解決策かいけつさくは数学科学すうがくかがくにはまったく属ぞくさない」と否定ひていしました。ケンブリッジ大学だいがくのG・スペンサー＝ブラウンも数学すうがくの歴史れきしを汚よごすものだと主張しゅちょうし、この手法しゅほうを「不正行為ふせいこうい」とみなしたある大学だいがくの数学科長すうがくかちょうは、大学院生だいがくいんせいの意欲いよくをそぐとして2人にんに会あうことを禁きんじたほどでした。

一方いっぽうで、この証明しょうめいを受うけ入いれた数学者すうがくしゃもいました。発表前はっぴょうまえは学術誌がくじゅつしで手法しゅほうに疑義ぎぎを呈ていしていた伝説的でんせつてきな数学者すうがくしゃウィリアム・トーマス・タットは発表はっぴょうを受うけて2人にんを祝福しゅくふくし、ドイツのハインリヒ・ヘーシュも自身じしんがアルゴリズム的てきな手法しゅほうを考案こうあんしていたため受うけ入いれました。証明しょうめいの作成さくせいを手伝てつだったハーケンの息子むすこによれば、数学者すうがくしゃたちの反応はんのうは世代せだいで大おおきく分わかれたといいます。40歳以上さいいじょうの人々ひとびとはコンピューターによる証明しょうめいが正ただしいと納得なっとくできなかった反面はんめん、40歳未満さいみまんの人々ひとびとは700ページにわたる手動しゅどうでの計算けいさんのほうが信用しんようできないと感かんじていたと証言しょうげんしています。

四色定理よんしょくていりをめぐっては、2026年ねんにも日本にほんやデンマークの研究けんきゅうチームによって新あらたな証明しょうめいが発表はっぴょうされ、グラフを4色しょくで塗ぬり分わけるアルゴリズムが大幅おおはばに高速化こうそくかされました。コンピューターによる「証明しょうめい」がもたらした半世紀前はんせいきまえの分断ぶんだんは、テクノロジーの発展はってんに伴ともなって数学界すうがくかいが直面ちょくめんした大おおきな課題かだいとして、今いまなお語かたり継つがれています。