距離1の2点を違う色に塗るには、平面では6色以上必要

この記事の要点

問題: 平面のすべての点に色を塗り、ちょうど距離1だけ離れた2点は必ず違う色にします。最低で何色あれば塗れるでしょうか。
四色定理との違い: 地図の国ではなく、平面の一つひとつの点を塗る問題です。「地図は4色で塗り分けられる」という四色定理とは別の問題で、こちらは4色では足りません。
これまで: 7色あれば塗れることは1950年ごろから知られていました。必要な色数の下限は、2018年に「4色では足りない」と分かったところで止まっていました。
今回: OpenAIのモデルが書いた論文で、「5色でも無理」が証明されました。答えは6か7のどちらかに絞られます。
確かさ: 主定理は定理証明支援系Leanで形式化されたと公開リポジトリに記載されています。論文は査読前です。

この記事で読む論文

The Euclidean plane is not five-colorable

OpenAI　2026年9月23日付　プレプリント（査読前）　PDF 450KB

論文のPDFを読む GitHubで見る（LaTeXソース・BibTeX） Leanの形式化を見る

PDFは2026年10月6日にGitHubで公開された版のコピーで、Apache License 2.0（全文）に従って掲載しています。修正版が出た場合は、GitHubのほうが新しくなります。

もう少し詳しくは大学1〜2年程度の数学、専門的な話は論文の中身に踏み込む補足です。どちらも開かずに読み進められます。

OpenAIが722本の数学論文を公開

2026年10月6日、OpenAIは未公開の社内モデルが書いた数学の論文をGitHubで公開しました^[1]。収録されているのは722本で、関連する論文をまとめた372の「ファミリー」に分類されています。整数論、代数幾何、組合せ論、数理物理など17分野にわたり、長年の未解決問題に決着をつけたと主張するものも含まれています。

この記事では、その中から問題文を中学生でも理解できる結果を一つ取り上げます。「平面を何色で塗り分けられるか」という、70年以上前に出された問題です。

どんな問題か

平面上のすべての点に色を塗ります。ルールは一つだけで、ちょうど距離1だけ離れた2点は違う色にすることです。距離が1でなければ、同じ色でも違う色でも構いません。

図1　中心の点を青で塗ると、そこから距離1の円周上の点はすべて青以外にしなければなりません。

色の数をできるだけ少なくしたいとき、最低で何色必要か。この最小の色数を平面の彩色数と呼び、 $\chi(\mathbb{R}^2)$ と書きます。1950年にエドワード・ネルソンが考えた問題で、ハドヴィガー＝ネルソン問題とも呼ばれます^[2,3]。

この問題では、塗り方に制限がありません。色の境目がどれほど入り組んでいても、1点ごとに好きな色を選んで構いません。この「何でもあり」の自由さが、あとで証明を難しくする原因になります。

もう少し詳しく数式での定義とグラフの言葉

$k$ 色での塗り分けとは、写像 $c:\mathbb{R}^2\to\{1,\dots,k\}$ で次をみたすものです。

\|x-y\|=1 \;\Longrightarrow\; c(x)\neq c(y) \qquad (x,y\in\mathbb{R}^2).

平面のすべての点を頂点とし、距離がちょうど1の2点を辺で結んだグラフを単位距離グラフと呼びます。 $\chi(\mathbb{R}^2)$ は、このグラフの彩色数（隣り合う頂点が同じ色にならない塗り方に必要な最小の色数）です。頂点は非可算無限個あり、辺どうしは交差しても構いません。

写像 $c$ には可測性も連続性も課しません。色ごとの点の集まり $A_i=c^{-1}(i)$ は、面積を測れないような集合でも構いません。

四色定理との違い

「色の塗り分け」「4色、5色」と聞くと、四色定理を思い浮かべる人も多いと思います。四色定理は「どんな地図も、隣り合う国が違う色になるように4色で塗り分けられる」という定理です。1976年にAppelとHakenがコンピュータを使って証明し^[4]、2005年にはGonthierらが定理証明支援系Coqで証明を形式化しました^[5]。

この記事の問題は、名前は似ていますが別の問題です。塗るものと、違う色にしなければならない組が違います。

	四色定理	この記事の問題
塗るもの	地図の国（ひとまとまりの領域）	平面の一つひとつの点
違う色にする組	境界線を共有する2つの国	ちょうど距離1だけ離れた2点
必要な色数	4色で足りる	6色か7色（5色では足りないことが今回証明された）
解決したか	1976年に解決	未解決

四色定理では、遠く離れた国どうしは同じ色で構いません。一方、この記事の問題では、どの点にとっても、半径1の円周上にあるすべての点が「違う色にしなければならない相手」になります（図1）。制約がずっと多いので、4色で足りないことは1950年ごろから分かっていました。

2色でも3色でも足りない

まず、少ない色では足りないことを確かめます。一辺の長さが1の正三角形を平面のどこかに置くと、3つの頂点は互いに距離1です。3点とも違う色にする必要があるので、2色では足りません。

図2　一辺1の正三角形の3頂点は、すべて違う色になります。

3色で足りないことは、モーザーのスピンドルと呼ばれる7点の図形で分かります^[6]。正三角形を2枚つなげたひし形を考えます。左下の点Aを青とすると、ひし形の残りの2点はオレンジと緑になるので、遠い側の先端Dは青に戻るしかありません。

同じひし形をもう一つ、点Aを共有したまま少し回して置くと、その先端D′も青になります。ここで、2つの先端DとD′の距離がちょうど1になる角度まで回しておけば、距離1の2点がどちらも青になってしまいます。3色ではどう塗っても矛盾するので、少なくとも4色が必要です。

図3　モーザーのスピンドル。黒と赤の線はすべて長さ1です。3色で塗ると、2つの先端が同じ色になってしまいます。

もう少し詳しく2つのひし形をどれだけ回すか

一辺1のひし形（正三角形2枚）の長い対角線の長さは $\sqrt{3}$ です。点Aを中心に2つのひし形を角度 $\theta$ だけずらすと、先端どうしの距離は $2\sqrt{3}\sin(\theta/2)$ になります。これが1になるのは

\theta = 2\arcsin\frac{1}{2\sqrt{3}} \approx 33.56^\circ

のときです。こうしてできる図形は7頂点・11辺の単位距離グラフで、3色では塗れません。この図形は、今回の論文でも証明の最後の段階で使われます。

7色あれば塗れる

反対に、7色あれば塗り分けられます。平面を正六角形のタイルで敷き詰め、下の図のように7色を規則的に割り当てます。アイスベルが見つけた塗り方です^[2,3]。

ポイントは六角形の大きさです。一枚の六角形の差し渡しを1より少し短くしておけば、同じタイルの中の2点は距離1になりません。さらに、同じ色のタイルどうしは1より離れるので、同じ色の2点が距離1になることもありません。

両端は違う色です

図4　黒い線は長さ1の針です。両端の丸をドラッグして動かしてみてください。7色の塗り方では、針をどこに置いても両端は違う色になります。「5色（失敗例）」に切り替えると、両端が同じ色になる置き方が見つかります。

こうして、1950年ごろには $4\le\chi(\mathbb{R}^2)\le7$ まで分かりました。ここから先は長いあいだ動きませんでした。

もう少し詳しく六角形の大きさと色の決め方

今回の論文に書かれている数値で確かめます^[7]。六角形の外接円の半径を $r=2/5$ にとります。六角形の中心は三角格子をなし、隣り合う中心の距離は $\sqrt{3}\,r$ です。

平面を複素数平面とみて、 $\omega=e^{2\pi i/3}$ とおくと、中心の集合は $\mathbb{Z}+\mathbb{Z}\omega$ を $\sqrt{3}\,r$ 倍したものです。 $2-\omega$ を掛けて得られる部分格子は、 $|2-\omega|^2=7$ なので指数7です。中心をこの部分格子による7つの剰余類で色分けし、各点にはその点を含む六角形の色を塗ります。

具体的には、 $\mathbb{Z}[\omega]/(2-\omega)$ では $\omega\equiv2$ なので、中心 $a+b\omega$ の色は $a+2b \bmod 7$ で決まります。図4もこの式で塗っています。

同じ六角形の中の2点の距離は $2r=0.8<1$ 以下です。
同じ色の中心どうしは少なくとも $\sqrt{7}\cdot\sqrt{3}\,r=\sqrt{21}\,r$ 離れています。
したがって、同じ色の別々の六角形にある2点は $(\sqrt{21}-2)\,r\approx1.033>1$ 以上離れています。

境界上の点は、接するどちらかの六角形の色にすれば問題ありません。図4の5色版は、同じ式を $\bmod 5$ に変えただけの塗り方です。同じ色の中心が $\sqrt{3}\cdot\sqrt{3}\,r=1.2$ しか離れない組ができるので、ちょうど距離1の同色の組が現れます。

70年近く動かなかった下限

4と7のあいだのどこかが答えです。上限の7については、六角形よりうまい塗り方が見つかっていません。下限の4を5に上げるには、モーザーのスピンドルのような「4色では塗れない図形」を見つければ十分ですが、これが長年見つかりませんでした。

2018年、Aubrey de Greyが1581個の頂点をもつ単位距離グラフを構成し、4色では塗れないことをコンピュータで確かめました^[8]。その後、グラフはより小さくなり（Heuleの553頂点^[9]、Partsの509頂点^[10]）、別証明^[11]や人の手で確かめられる証明^[12]も出ています。これで $5\le\chi(\mathbb{R}^2)$ になりました。

1950年ごろ

ネルソンとアイスベル

2018年

de Greyの1581頂点のグラフ

2026年

今回の論文

図5　平面の彩色数として残っている候補の推移です。

一方、塗り方に条件をつけた版の問題は、別の道すじで調べられてきました。色の集まりの面積が測れる（可測な）塗り方に限ると、1981年にFalconerが5色以上必要なことを示しています^[13]。色の境目が地図のように整った塗り方なら6色以上必要で^[14,15]、多角形を貼り合わせた塗り方なら7色必要だと2025年に示されました^[16]。ただし、どれも「塗り方に条件をつければ」という話で、条件のない本来の問題には使えませんでした。

もう少し詳しく有限の図形で十分な理由と、可測性の壁

de Bruijn–Erdősのコンパクト性定理^[17]によれば、有限の $k$ について、グラフが $k$ 色で塗れることと、そのすべての有限部分グラフが $k$ 色で塗れることは同値です。したがって「平面は5色で塗れない」は「5色で塗れない有限の単位距離グラフが存在する」と同値です。このグラフを具体的に示さなくても、存在さえ示せれば下限は上がります。今回の論文もこの形で、5色で塗れない有限グラフが存在することは分かりますが、そのグラフは具体的には示されていません。

可測な塗り方と一般の塗り方の違いは見かけ以上に大きいものです。Payne^[18]は、辺の向きが「成分が有理数の単位ベクトル」に限られた単位距離グラフを考えました。このグラフは一般の塗り方なら2色で塗れますが、可測な塗り方では5色以上必要です。距離の制約が同じに見えても、可測性を仮定した結果をそのまま一般の塗り方に移すことはできません。

今回の結果

OpenAIが公開した論文「The Euclidean plane is not five-colorable」（2026年9月23日付、PDF）は、条件をつけない本来の問題で次を証明したと主張しています^[7]。

定理1 OpenAI, 2026

平面をどのように5色で塗っても、同じ色でちょうど距離1の2点が必ず存在する。色の集まりにはどんな正則性も仮定しない。したがって

6\le\chi(\mathbb{R}^2)\le7.

2018年以降の進展は、塗れない図形をコンピュータで探す方向でした。今回の証明は図形を探すのではなく、解析学・確率論・位相幾何学を組み合わせた議論で直接示しています。冒頭で述べた「何でもあり」の塗り方を、どうやって扱える形に持ち込むかが中心になります。

証明の考え方

証明は背理法です。5色の正しい塗り方があると仮定して、矛盾を導きます。大きく二つの段階に分かれています。

1
どんな塗り方も「測れる」塗り方に置き換える
任意の正しい塗り方から、面積が測れて、ほとんどすべての距離1の組で色が違う塗り方を作る。色の数によらず成り立つ。
2
円周上の色の並びを調べる
各点を中心とする半径1の円の上で色がどう並ぶかを見ると、ほとんどの方向で現れる色は2色以下になる。
3
色の境目から「色の輪」を取り出す
色の境目をたどると、3色・4色・5色のどれかが輪のようにつながった構造が必ず見つかる。
4
どの輪もありえないことを示す
5色と4色の輪は角度の議論で否定する。3色の輪からは3色だけの領域ができ、そこにモーザーのスピンドルを置くと矛盾する。

第1段階は、条件をつけた版の問題で使われてきた道具を、本来の問題に持ち込むための部分です。でたらめな塗り方には面積も密度も使えないので、まず平均をとる操作で「測れる」塗り方に移します。代わりに、距離1の組がすべて違う色という条件は「ほとんどすべての組で違う色」に弱まります。論文は、この弱い条件の塗り方が存在することと、本来の正しい塗り方が存在することが同値だと示しています。

第2段階では、その弱い5色塗りが存在しないことを示します。面白いのは最後の一手で、3色しか使えない領域ができてしまえば、前半で紹介したモーザーのスピンドルをそこに置くだけで矛盾が出ます。1961年の小さな図形が、2026年の証明の締めくくりに使われているわけです。

もう少し詳しく「弱い可測な塗り方」の定義

$S^1$ を単位円、 $\sigma$ をその上の正規化された弧長測度とします。ルベーグ可測な写像 $c:\mathbb{R}^2\to\{1,\dots,k\}$ で、色の集まりを $A_i=c^{-1}(i)$ とおいたとき、すべての $R>0$ について

\sum_{i=1}^{k}\int_{B(0,R)}\int_{S^1}\mathbf{1}_{A_i}(x)\,\mathbf{1}_{A_i}(x+u)\,d\sigma(u)\,dx=0

をみたすものを弱い可測 $k$ 色塗りと呼びます。左辺は「点 $x$ と、そこから距離1の点 $x+u$ が同じ色になる組の量」を測っています。これが0であるとは、そうした組が測度0しかないということです。例外の組は許されます。

論文の転送定理は、すべての正の整数 $k$ について次が成り立つと述べています。

正しい $k$ 色塗りが存在する $\iff$ 弱い可測 $k$ 色塗りが存在する

逆向き（ $\Leftarrow$ ）は比較的短く示せます。ルベーグの密度定理から、自分の色の密度が1の点（論文の用語ではtypical point）どうしは、距離1なら違う色になります。任意の有限の図形を平行移動してこうした点の上に載せられるので、有限グラフはすべて $k$ 色で塗れます。あとはコンパクト性定理で平面全体の正しい塗り方が得られます。この部分は、FalconerやPayneの密度点の議論を応用したものです。

難しいのは前向き（ $\Rightarrow$ ）で、次の「専門的な話」で扱います。

専門的な話転送定理：ハール測度の剛性

$F=\overline{\mathbb{Q}}\cap\mathbb{R}$ （実代数的数）、 $E=F(i)$ （「代数的な平面」）、 $K=\{u\in E:|u|=1\}$ （代数的な回転の群）とおきます。 $E$ は可算なので、与えられた正しい塗り方を $E$ に制限し、平行移動と回転で平均をとると、 $E$ の正しいラベル付け全体の上の不変な確率法則が得られます（従順群上の平均化）。この種の不変なランダム化は、確率版のハドヴィガー＝ネルソン問題でも使われてきました^[19,20]。

ここで問題になるのは、得られる関数が $E$ 上にしかなく、平面の位相とつながっていないことです。そこで、離散加法群 $E$ の指標全体のなすコンパクト群 $D$ と、普通の連続な指標 $z\mapsto e^{i\xi\cdot z}\ (\xi\in\mathbb{R}^2)$ のなすボレル部分群 $C\subset D$ を考えます。不変法則の $L^2$ 上でスペクトル定理を使うと、各ラベルの指示関数は「 $C$ に台をもつ部分」と残りに分解されます。

中心となるのは次の剛性定理です。

定理2 野性的な指標法則の剛性

$D$ 上の $K$ 不変な確率測度 $\nu$ で $\nu(C)=0$ をみたすものは、ハール測度に限る。

ハール測度のフーリエ係数は0でない点ですべて消えるので、「残り」の部分は0でない代数的な平行移動に対して相関をもちません。したがって、残りを取り除いても距離1の組での相関が0であることは保たれます。一方、 $C$ に台をもつ部分への射影はある因子への条件付き期待値なので、非負性と「ラベルの成分の和が1」が保たれ、平行移動は $\mathbb{R}^2$ 全体へ連続に延長できます。可測な版を選んで各点で正の成分をもつ最小のラベルを選べば、弱い可測塗りが得られます。

剛性定理の証明では、Furstenberg–Zimmerのコンパクト拡大の手法^[21]で因子の塔を作ります。その塔に沿って $C$ の測度が0のまま保たれること（相対特異性）を示し、半径方向の関数に関する差分不等式と、有限次の数体を使った議論で、0でない半径でのフーリエ係数が消えることを導きます。

専門的な話5色の否定：パレット、色の輪、連続体

弱い可測5色塗りがあると仮定します。中心 $x$ を固定し、 $y\to x$ 、 $r\to1$ としたときの円周上の色の標本 $e\mapsto(\mathbf{1}_{A_i}(y+re))_{i=1}^{5}$ の弱*極限を考えます。方向 $e$ で正の重みをもちうるラベルの集まりをパレット $P_x(e)$ と呼びます。

パレットの大きさ：すべての中心 $x$ について、ほとんどすべての $e$ で $1\le|P_x(e)|\le2$ （論文の第5節）。円周上の測度のフーリエ変換の減衰を使い、色の境目の滑らかさや有限周長は仮定しません。
遷移グラフ：各中心で、ラベル間の遷移を記録した有限グラフ $\Gamma_x$ を作ります。 $\Gamma_x$ が閉路を含む中心の集合は閉かつ局所有限です（第6節）。
連続体の抽出：色の指示関数を円板平均でなめらかにし、しきい値処理すると、小さな円板を除いて完全グラフ $K_5$ への連続写像が得られます。閉路をもつ中心から離れたところでは森の構造を使って穴を埋め、平面の被覆に関する障害から、ある円板のまわりで非自明なループが生じます。そこから長さ $\ell\in\{3,4,5\}$ の単純なラベルの閉路と、各辺に対応するコンパクト連結集合 $K_j$ （共通の点 $x$ をもつ）が取り出せます（第7節）。

各 $K_j$ について、辺の両端のラベルは次の開集合でほとんどいたるところ現れません。

\Delta(K)=\Bigl\{z:\min_{q\in K}|z-q|<1<\max_{q\in K}|z-q|\Bigr\}.

図6　連結な集合

K

に対する

\Delta(K)

は、

K

の各点を中心とする半径1の円が通る範囲です。

このように連結な集合から距離の除外を引き出す考え方は、多角形の塗り方を扱ったSokolov–Voronovの議論^[16]に先例があります。今回の論文では、その連結集合を仮定せず、測度の評価と位相的な抽出から作り出している点が異なります。

最後に、各 $K_j$ を $x$ に近づく点列の極限方向から、単位円のすぐ内側と外側で許されるラベルを決めます（第8節）。

長さ5：6か所の角度の語が両立しません。
長さ4：2組の対蹠的な方向が生じ、ありえない偶奇の規則が出ます。
長さ3：外側の2ラベルが6つの扇形で交互に並ぶことが強制され、3ラベルしか使わない開領域が残ります。有理数で与えた配置で、モーザーのスピンドルの7頂点をすべてこの領域に置けるので、矛盾します。

証明からは、次の確率的な性質も導かれます。ある定数 $\delta>0$ があり、例えば周期的で可測な5色塗りでは、長さ1の針をでたらめに落としたとき、両端が同じ色になる確率がつねに $\delta$ 以上になります^[7]。周期的な塗り方をどう工夫しても、失敗の割合を0に近づけることはできません。ただし $\delta$ の具体的な値は分かっていません。証明が、5色で塗れない有限グラフの存在を示すだけで、そのグラフを具体的に与えないためです。

どこまで確かなのか

AIが書いた論文なので、どこまで信用できるかは気になるところです。現時点で分かっていることを整理します。

論文は2026年9月23日付のプレプリントで、査読はまだです^[7]。
リポジトリの形式化カタログには、この論文の主定理がLeanで形式化された結果として登録されています。宣言名は OAI.EuclideanFiveColor.no_proper_five_coloring です^[22]。
検証の設定ファイルで許可されている公理は、Leanで標準的に使う propext、Quot.sound、Classical.choice の3つです。
リポジトリのREADMEは、形式化されていない結果には問題が含まれうると注意しています。この結果は形式化されている側に入ります。

Leanでの主張は次のとおりです。複素数平面 $\mathbb{C}$ から5色への写像で、距離1の2点を必ず違う色にするものは存在しない、と読めます。

def ProperColoring (colorCount : ℕ) (coloring : ℂ → Fin colorCount) : Prop :=
  ∀ point otherPoint : ℂ, ‖point - otherPoint‖ = 1 → coloring point ≠ coloring otherPoint

theorem no_proper_five_coloring : ¬ ∃ coloring : ℂ → Fin 5, ProperColoring 5 coloring

リポジトリの記載どおりなら、この主張の証明は計算機で検査済みということになります。一方で、定義が意図どおりかは人が読んで確かめる必要があります。この主張は短く、上のとおり問題文そのものです。なお、筆者はこの記事を書いた時点で、Leanの検査を手元で再実行していません。

残された問題

答えは6か7のどちらかになりました。6色で塗れる方法があるのか、それとも7色が必要なのかは分かっていません。7色を示すには「6色では塗れない」ことを証明する必要があり、6色を示すには六角形の塗り方より上手な塗り方を見つける必要があります。

AIと数学について

リポジトリの説明によれば、OpenAIは既存の数学の評価で性能が頭打ちになったため、未解決問題での評価を広げました^[1]。モデルに出した問題はおよそ4,000問で、結果の多くは同じ手順で得られ、1件あたり平均3時間ほどの思考時間を使ったとされています。意義のある結果に絞り込んだものが、今回の722本です。

今回の論文を読むと、de Bruijn–Erdősのコンパクト性定理、Falconerの密度点の議論、Furstenberg–Zimmerの構造理論、Sokolov–Voronovの境目の議論、そしてモーザーのスピンドルと、数十年にわたる人の仕事の上に組み立てられていることが分かります。こうした論文が査読や形式化を経てどう受け止められていくのか、引き続き追いかけていきます。

参考文献

OpenAI, openai/math: mathematical manuscripts and supporting proof artifacts, GitHub, 2026.
A. Soifer, The 50th Anniversary of One Problem: The Chromatic Number of the Plane & Its Relatives. Part 1, Mathematics Competitions, 2003.
H. Hadwiger, Ungelöste Probleme Nr. 40, Elemente der Mathematik 16, 1961.
K. Appel, W. Haken, Every planar map is four colorable. Part I: Discharging, Illinois Journal of Mathematics 21(3), 1977.
G. Gonthier, Formal Proof: The Four-Color Theorem, Notices of the AMS 55(11), 2008.
L. Moser, W. Moser, Solution to Problem 10, Canadian Mathematical Bulletin 4(2), 1961.
OpenAI, The Euclidean plane is not five-colorable, OpenAI Math Release preprint, September 23, 2026.
A. D. N. J. de Grey, The Chromatic Number of the Plane Is at Least 5, Geombinatorics 28(1), 2018.
M. J. H. Heule, Computing Small Unit-Distance Graphs with Chromatic Number 5, Geombinatorics, 2018.
J. Parts, Graph Minimization, Focusing on the Example of 5-Chromatic Unit-Distance Graphs in the Plane, Geombinatorics, 2020.
G. Exoo, D. Ismailescu, The Chromatic Number of the Plane Is at Least 5: A New Proof, Discrete & Computational Geometry, 2020.
J. Parts, The Chromatic Number of the Plane Is at Least 5: A Human-Verifiable Proof, Geombinatorics, 2020.
K. J. Falconer, The Realization of Distances in Measurable Subsets Covering ℝⁿ, Journal of Combinatorial Theory, Series A, 1981.
D. R. Woodall, Distances Realized by Sets Covering the Plane, Journal of Combinatorial Theory, Series A 14, 1973.
S. P. Townsend, Colouring the Plane with No Monochrome Units, Geombinatorics 14(4), 2005.
G. Sokolov, V. Voronov, On the Chromatic Number of the Plane for Map-Type Colorings, arXiv, 2025.
N. G. de Bruijn, P. Erdős, A colour problem for infinite graphs and a problem in the theory of relations, Indagationes Mathematicae 13, 1951.
M. S. Payne, Unit Distance Graphs with Ambiguous Chromatic Number, The Electronic Journal of Combinatorics 16, 2009.
T. Bourgeat, M. Heinrich, P. Melotti, J.-M. Robert, A probabilistic Hadwiger–Nelson problem, arXiv, 2015.
H. Gwyn, J. Stavrianos, A Finite Graph Approach to the Probabilistic Hadwiger–Nelson Problem, Geombinatorics, 2022.
H. Furstenberg, Ergodic behavior of diagonal measures and a theorem of Szemerédi on arithmetic progressions, Journal d'Analyse Mathématique, 1977.
OpenAI, Lean formalization: OAI/Geometry/PlaneColoring/Five.lean, openai/math, 2026.