サイエンス

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


どんな地図でも隣り合う地域を同じ色にしないように4色だけで塗り分けられるという「四色定理」について、日本やデンマークなどの研究者からなるチームが新たな証明を発表しました。今回もコンピューターを利用した証明ですが、従来とは異なる場所に着目することで、多数の処理をまとめて行えるようになり、実際にグラフを4色で塗り分けるアルゴリズムも大幅に高速化されていると、科学系メディアのQuanta Magazineが解説しています。

[2603.24880] The Four Color Theorem with Linearly Many Reducible Configurations and Near-Linear Time Coloring
https://arxiv.org/abs/2603.24880

The Four-Color Theorem Gets a Rare New Proof | Quanta Magazine
https://www.quantamagazine.org/the-four-color-theorem-gets-a-rare-new-proof-20260910/

四色定理の始まりは1852年で、イギリスの数学者フランシス・ガスリーがイングランドの州を地図上で塗り分けていた際、「境界線を共有する地域が同じ色にならないようにするには、どんな地図でも4色あれば十分なのではないか」と気づいて提起しました。この問題は一見すると子どもでもわかるレベルで単純ですが、実際にあらゆる地図について4色で十分であることを数学的に証明するのは極めて困難でした。

この問題を数学的に扱うため、地図は「グラフ」と呼ばれる形に置き換えられます。このグラフは学校の数学で教わるグラフのことではなく、それぞれの地域を点、つまり「頂点」で表し、境界線を共有する2つの地域に対応する頂点を線、つまり「辺」で結んで表現した図形です。グラフを活用することで、四色問題は「線で結ばれている頂点同士を異なる色にしながら、すべての頂点を4色以内で塗れるか」という問題になります。

by MathPage

1879年には数学者アルフレッド・ブレイ・ケンプが証明に成功したと発表しました。ケンプは「もし4色では塗れないグラフがあるなら、その中で最も小さいものを考える」という発想を採用しました。そこから頂点を1つ取り除けば、より小さなグラフになるため4色で塗れるはずだというわけです。そこで、残ったグラフの一部の色をうまく入れ替えれば、取り除いた頂点を戻しても4色で塗れることを示そうとしました。

しかし1890年、パーシー・ジョン・ヒーウッドによってケンプの証明には誤りがあることが明らかになりました。それでも、2色でつながった頂点の集まりの色を入れ替える「ケンプ鎖」という考え方自体は有用で、その後の正しい四色定理の証明にも引き継がれました。


正しい証明が登場したのは1976年です。ケネス・アッペルとヴォルフガング・ハーケンは、平面グラフの中には必ず特定の「配置」が含まれており、それを利用すれば問題をより小さいグラフへ縮小できることを利用しました。このように、そこが存在すれば四色定理の最小の反例にはなり得ないと示せる局所的な構造を「可約配置」と呼びます。

簡単にいえば、「どんな巨大なグラフでも、必ずどこかに攻略可能な小さなパターンがある」ことを示し、そのパターンを取り除いて小さな問題を解き、最後に元へ戻していくという方法です。アッペルとハーケンは調べるべき候補を1482種類まで絞り込み、それぞれが実際に可約であることをコンピューターで確認しました。これによって、提唱から120年以上を経て四色定理が初めて証明されました。

Every planar map is four colorable
https://projecteuclid.org/journals/bulletin-of-the-american-mathematical-society/volume-82/issue-5/Every-planar-map-is-four-colorable/bams/1183538218.full


ただし、膨大な場合分けの一部を人間ではなくコンピューターが確認していたため、「計算機の動作を完全に追跡できない証明を数学的証明と呼べるのか」という疑問が呈され、この証明は当時大きな論争を引き起こしました。その後1997年には、ニール・ロバートソンらの研究チームがアッペルとハーケンの方法を整理し、コンピューターで確認する配置を633種類まで減らした、より単純な証明を発表しました。コンピューターを利用した数学的証明も広く受け入れられるようになっていたことから、この証明は数学界でも速やかに受け入れられました。


1976年と1997年の証明には、「巨大なグラフを実際に4色で塗る場合、『処理可能な配置を1つ探す』『その部分を取り除いてグラフを少し小さくする』『再び処理可能な配置を1つ探す』という操作を繰り返す」という共通点があります。これはいわば、大きな荷物の山から毎回1個だけ取り除き、そのたびに山全体を調べ直すようなものだといえます。

例えば頂点がn個あるグラフの場合、この方法による彩色アルゴリズムの処理にはO(n2)程度の多項式時間が必要でした。これはグラフの頂点数がn倍になると、検証に必要な計算量がおおむねnの2乗に比例して増えていくことを示します。


国立情報学研究所の河原林健一氏、東京大学の井上裕太氏と宮下篤之氏、サイモンフレーザー大学のボヤン・モハル氏、デンマーク工科大学のカーステン・トマセン氏、コペンハーゲン大学のミッケル・トルップ氏からなる研究チームは、この問題に別の方向から取り組みました。

従来の証明では周囲とのつながりが比較的少ない頂点が集まる場所を中心に処理可能な配置を探していましたが、河原林氏らの研究チームは各頂点が6つの頂点につながり三角形が規則的に並ぶような、これまであまり利用されてこなかった「平らな領域」にまで探索対象を広げました。

その結果、研究チームは8202種類という大規模な配置の集合を見つけました。数だけを見れば1997年の633種類より大幅に増えているため、一見すると証明が複雑になったように見えます。しかし重要なのは、その中から互いに干渉しない多数の配置を同時に処理できることです。

たとえるなら、従来の方法は大量の荷物がある部屋で「捨てられる物を1つ探す」「1つ捨てる」「また部屋全体から1つ探す」という作業を繰り返すようなものだったのに対して、新しい方法は互いに邪魔にならない「捨てられる物」を一度に大量に見つけられるため、1回の処理で部屋の荷物を一定割合ずつ減らしていくことができます。

この違いによって、1回の処理でグラフから一定割合の頂点を減らせるようになります。例えば、毎回数個だけ減らす場合はグラフが空になるまで大量の繰り返しが必要ですが、毎回一定割合ずつ減らせるなら、1000個、500個、250個というように急速に問題を小さくできます。その結果、4色で塗り分けるための計算量は従来のO(n2)からO(nlog_n)へと改善されました。研究チームはこれを「near-linear time」、つまりほぼ線形時間の4色彩色アルゴリズムと位置付けています。

今回の成果は、「四色定理が正しい」という結論そのものを変えるものではありません。また、コンピューターを使わずに誰でも短時間で確認できるような簡潔な証明が見つかったわけでもなく、むしろコンピューターで確認する配置の数は以前より増えています。河原林氏らによる新証明は、平面グラフには一度に多数の場所を処理できる構造が潜んでいることを明らかにし、その性質を使って四色定理を再証明するものです。

この性質は四色定理以外にも応用できる可能性があります。研究チームが着目した「平らな領域」は平面グラフだけでなく、ドーナツ状のトーラスなど別の曲面上に描かれる大規模なグラフにも現れるため、新たに開発された手法が曲面上のグラフの彩色問題をはじめとする別のグラフ理論の問題を解く道具になることも期待されています。一方で、トマセン氏は「今回の成果を得た後も、最終的には『コンピューターを使わず、なぜ4色だけで十分なのかを理解できる証明』を見つけたい」と語っています。

・関連記事
16人の数学者がAIの精度や信頼性など数学分野への潜在的な脅威について警告する「ライデン宣言」を発表 - GIGAZINE

OpenAIが「GPT-6 Astraより高性能なモデル」を用いて数学の難問「ナビエ・ストークス方程式」の解決を主張、一方で人間の数学者の成果を流用した疑惑も生じる - GIGAZINE

数学の難問を与えられた100体のAIエージェントが不正を行う側と不正に対抗する側に分かれたことがGoogleの実験で判明 - GIGAZINE

Claudeがフェルマーの最終定理を11日で形式化、1300万行のLeanコードで初の完全な機械検証済み証明を完成 - GIGAZINE

AI支援で作られた「コラッツ予想の反証」は無効、Leanのカーネルバグを突いていたことが判明 - GIGAZINE

in サイエンス, Posted by log1i_yk

You can read the machine translated English article A new proof of the Four Color Theorem ha….