AIが塗り分けパズルを解く
線で結ばれた点のネットワーク、数学者がグラフと呼ぶものを考えよう。そこで、線で結ばれた2点が決して同じ色にならないように点を塗り分ける。これを可能にする最小の色数が、そのグラフの彩色数だ。有名な特別な場合が1977年に証明された四色定理で、その論文の題名がすべてを物語っている。「すべての平面地図は四色で塗り分けられる(Every planar map is four colorable)」。
ハドヴィガーの1943年の賭け
1943年、ハドヴィガーはすべてのグラフについての壮大な規則を提案した。点や線を消したり、線で結ばれた2点を一つにまとめたりしてグラフを縮める。その結果をマイナーと呼ぶ。ハドヴィガーは、こうして得られる最大の完全グラフ、すなわちすべての点が他のすべての点と結ばれた集まりに注目し、必要な色数がその集まりの大きさを超えることはないと予想した。
論文はこれを「グラフ理論で最も古く、最も根本的な問題の一つ」と呼ぶ。証明されているのは小さな場合だけだ。集まりの大きさが5までなら、四色定理と同値か、四色定理に帰着できることがわかっている。6からは未解決だ。
対数一つずつ迫っていく
正確な主張が手ごわいので、研究者たちは色数を集まりの大きさの何らかの関数で、それもできるだけゆっくり増える関数で抑えようとしてきた。論文はその進歩をたどる。何十年ものあいだ、最良の上界は比例よりわずかに速く増えていた。対数の平方根を含む因子の分だけだ。数年前、ノリン(Norin)、ポストル(Postle)、ソン(Song)がその壁を破った。続いてデルクール(Delcourt)とポストルがそれをさらに改良し、決定的なことに、かなり小さなグラフを扱えば十分であることを示した。リウ(Liu)とルオ(Luo)は、余分な因子を三重対数まで押し下げた。
自然な終着点は線形ハドヴィガー予想だ。集まりの大きさの一定倍があれば、いつでも足りる。モントリオールのマギル大学のセルゲイ・ノリン(Sergey Norin)と、チューリッヒ工科大学(ETH Zurich)のラファエル・シュタイナー(Raphael Steiner)が、いまこれを証明したと主張している。
機械が果たした役割
著者らは明言している。証明を見つけたのは、彼らの指示に従ったOpenAIのモデル、GPT-6 Astraだった。 彼らはまず、欠けている一片だと考えていた、非常に密なグラフの場合を証明するよう求めた。AIは成功した。彼らの言葉では、「わずか数時間と、いくらかの励ましのあとで」。ある依存関係を明示するよう求めると、AIはある大きさまでのグラフをカバーした。しかし必要な範囲には少し届かなかった。そこで彼らは、その隙間を埋める独創的なアイデアを求め、それが最終的な証明の「ブートストラップ」の段階を生んだ。著者ら自身の具体的な証明のアイデアは、縮約に関する一つの提案を除いて、ほとんど残らなかったという。
文章を書いたのは人間だ。別のOpenAIのモデルが校正と参考文献の整理を手伝った。著者らによれば、OpenAIのCodexが、証明支援系Leanで証明全体の形式的な、機械で検証できる版を作成し、AIが書いた初期の草稿とともにオンラインで公開されている。数学についての全責任は著者らが負う。
証明の中身
議論は二つの半分からなる。
- 小さなグラフ、少ない色。 集まりの大きさの上限からそれほど大きくないグラフについて、著者らは集まりの大きさの約4倍で十分であることを示す。出発点は、リード(Reed)とシーモア(Seymour)による1998年の結果だ。彩色を緩めた「分数」版は、すでに因子2で線形の規則に従う。新しい研究は、グラフにいくつかの線を足し、補助的な構造のなかに巨大なマッチングを見つけることで、分数彩色を本物の彩色に変える。
- ブートストラップ。 二つ目の議論は、カバーされるグラフの大きさの範囲を、各段階で指数において3分の4倍に広げる。代償として定数は大きくなる。10段階で範囲は3分の1から約5.92まで広がり、デルクール=ポストルの帰着が求める閾値5を超える。この半分では、ギャルファーシュ(Gyárfás)による古い手法が使われる。著者らによれば、この問題に適用されたことはこれまでなかったという。
著者らはこの証明を、既知の道具から組み立てられたものと説明する。「既存の結果の凸包のなかに含まれている」が、その明らかな縁にあるわけではない、と。
残された問題
定数は途方もなく大きい。大まかな見積もりで約10¹⁰⁰だ。著者らは10¹⁰未満まで下げる余地があると見ているが、たとえば100に届かせるには新しいアイデアが必要だろうと考えている。ハドヴィガーの正確な予想には手がついていない。「私たちは決めかねている」と彼らは書く。論文はプレプリントであり、41ページの新しい数学は、これから他の専門家たちの精査を受けることになる。