ブールピタゴラス三つ組の問題

ブールピタゴラス三つ組問題は、正の整数を赤と青で色分けして、すべての要素が赤または青のピタゴラス三つ組にならないようにできるかどうかというラムゼー理論の問題です。ブールピタゴラス三つ組問題は、2016年5月にマリイン・ホイレ、オリバー・クルマン、ビクター・W・マレクによってコンピュータ支援証明によって解決され、そのような色分けは7824までしか不可能であることが示されました。^{[ 1 ]}

問題は、正の整数をそれぞれ赤または青に着色して、ピタゴラス数a、b、cが を満たさないようにできるかどうかを問うものです。${\displaystyle a^{2}+b^{2}=c^{2}}$すべて同じ色です。

例えば、ピタゴラス数 3、4、5 (${\displaystyle 3^{2}+4^{2}=5^{2}}$) 3と4が赤色の場合、5は青色でなければなりません。

マリイン・ホイレ、オリバー・クルマン、ヴィクター・W・マレクは、そのような彩色は7824までしか不可能であることを示した。証明された定理の実際の記述は次のとおりである。

7825までの数字には2 ⁷⁸²⁵ ≈ 3.63×10 ²³⁵⁵通りの塗り分けの組み合わせがあります。これらの塗り分けの組み合わせは、論理的かつアルゴリズム的に約 1 兆 (それでも非常に複雑) のケースに絞り込まれ、ブール充足可能性問題として表現されたこれらのケースは、 SAT ソルバーを使用して検証されました。証明の作成には、テキサス先端計算センターの Stampede スーパーコンピュータで 2 日間にわたって約 4 CPU 年分の計算が必要となり、200 テラバイトの命題証明が生成され、それが 68 ギガバイトに圧縮されました。

証明を記述した論文は、SAT 2016 会議で発表され、^{[ 2 ]}最優秀論文賞を受賞しました。^{[ 3 ]}下の図は、単色ピタゴラス数を持たない集合 {1,...,7824} の可能な彩色ファミリーを示しており、白い正方形は、この条件を満たしながら赤または青のいずれかに着色できます( OEISのシーケンスA383181 )。

1980年代にロナルド・グラハムは、この問題の解決に100ドルの賞金を提供し、現在ではマリイン・ホイレに授与されている。^{[ 1 ]}

2018年現在、この問題は2色以上の場合、つまり、どのピタゴラス数も同じ色にならないような正の整数のk彩色（k ≥ 3）が存在するかどうかについては未解決である。 ^{[ 4 ]}

• 長文の数学的証明一覧