Проблема трійок Буля — Піфагора

Проблема трійок Буля — Піфагора полягає у відповіді на питання, чи можна поділити множину натуральних чисел $\{1,2,3,...\}$ на дві частини так, щоб у кожній частині не було жодної піфагорової трійки. Марійн Гейле, Олівер Кульман та Віктор Марек 2016 року довели, що це можливо лише для $7824$ і менших чисел. Для множини з $7825$ чисел і більше такий поділ неможливий. Іншими словами, серед $7825$ натуральних чисел $\{1,2,3,...,7825\}$, розфарбованих у два кольори, завжди знайдеться монохроматична трійка $a$, $b$ і $c$ що $a^{2}+b^{2}=c^{2}$.

Рональд Грем разом із Ердешем сформулював проблему трійок Буля — Піфагора в публікації 1980 року

У стислій формі результат записується через число Радо для рівняння Піфагора: $R_{2}(a^{2}+b^{2}=c^{2})=7825$.

Проблема

Річард Радо

Проблема трійок Буля — Піфагора виникла в теорії Ремзі, головним мотивом якої є заперечення абсолютного хаосу в достатньо великих системах. Проблема стосується питання, чи можна поділити множину натуральних чисел $\{1,2,3,...\}$ на дві частини так, щоб кожна частина не мала жодної піфагорової трійки, тобто таких $a$, $b$ і $c$ що $a^{2}+b^{2}=c^{2}$. У термінах фарбування чисел проблема виглядає так: чи можна розфарбувати натуральні числа у два кольори щоби жодна піфагорова трійка не була монохроматичною. Основні роботи теорії Ремзі, що пов'язані з проблемою трійок Буля — Піфагора, включають теореми Шура, ван дер Вардена та Радо.

У 1980-х Рональд Грем запропонував приз у розмірі 100 доларів тому, хто розв'яже цю проблему . У 2007—2008 роках він нагадав, що проблема була сформульована ще в його публікації разом із Палом Ердешем 1980 року, зазначив про обмаль даних, щоб вирішити проблему в той чи інший спосіб, і за Ердешевою традицією пообіцяв премію (250 дол.) за результат.

$N=1344,1514$

У грудні 2008 року Джошуа Купер і Кріс Пойрел надрукували перший приклад розподілу множини натуральних чисел $\{1,2,3,...,1344\}$ на дві частини так, що кожна частина не мала жодної піфагорової трійки. На обчислення пішло сотні годин процесорного часу. Результат було представлено у вигляді панелі $53\times 25+19$ чорних і білих квадратиків. Квадратик із координатами ($p,q$) задавав колір числа $n=25q+p$. Числа збільшувались знизу до гори, потім зліва направо.

2012 року Вільям Кей застосував алгоритм Робіна Мосера та Габора Тардоса та знайшов розв'язок проблеми трійок для множини $\{1,2,3,...,1514\}$.

$R_{2}(a^{2}+b^{2}=c^{2})>6500$

У травні 2015 року Келлен Маєрс і Дорон Зілбергер оприлюднили роботу зі втілення алгоритму здійсненності булевих формул (SAT) для обчислення чисел Радо, зокрема, для проблеми трійок Буля — Піфагора. Вони запровадили поняття дійсного розфарбовування, яке дає можливість знайти нижню межу для числа Радо. У результаті комп'ютерних обчислювань Маєрс і Зілбергер знайшли, що число Радо $R_{2}(a^{2}+b^{2}=c^{2})>6500$, та опублікували сертифікат існування дійсного розфарбовування множини $\{1,2,3,...,6500\}$ у трьох формах:

1. Рядок довжиною $6500$ з елементів $\{0,1\}$ для позначення кольору всіх чисел у послідовності.
2. Два списки чисел, що показує, у яку з двох частин потрапило кожне число під час розбивки.
3. Панель $70\times 92+60$ червоних і синіх квадратиків, в якій нумерація квадратиків збільшується зліва направо, потім зверху донизу.

У наведеній нижче візуалізаційній панелі червоний колір замінено на жовтий.

$N=7664$

У травні 2015 року Джошуа Купер і Ральф Оверстріт розфарбували двома кольорами $7664$ натуральних чисел $\{1,2,3,...,7664\}$ так, що всі піфагорові трійки були різнокольоровими .

$N=7824;R_{2}(a^{2}+b^{2}=c^{2})=7825$

Марійн Гейле, Олівер Кульман та Віктор Марек у травні 2016 року вирішили проблему трійок Буля — Піфагора за допомогою теореми 1.

Теорема

Теорема 1. Множину натуральних чисел $\{1,2,3,...,7824\}$ можна поділити на дві частини так, щоб кожна частина не мала жодної піфагорової трійки, але це не можливо для $\{1,2,3,...,7825\}$.

Доведення

Доведенням першого твердження теореми став позитивний приклад розфарбування двома кольорами $7824$ натуральних чисел. Приклад проілюстровано панеллю $100\times 78+24$ квадратиків трьох класів: двох пофарбованих і нефарбованого. До нефарбованого класу належать числа, що не входять до жодної піфагорової трійки, та деякі числа з трійок, чий колір не має значення. Нижній рядок у панелі займають числа $\{1,2,3,...,100\}$, над ним — $\{101,...,200\}$ і так далі до верхнього рядка $\{7801,...,7824\}$.

…

Науковці провели попередній аналіз усіх $2^{7825}\approx 3{,}6\cdot 10^{2355}$ варіантів розфарбування $7825$ чисел та зменшили обсяг доведення другого твердження теореми до близько трильйона ($10^{12}$) здебільшого досить складних варіантів. Теорема була доведена шляхом перебору всіх знайдених варіантів, використовуючи розв'язувач класу SAT Solver на 800 ядерному суперкомп'ютері Stampede у Комп’ютерному центрі Техаського університету протягом двох днів. Розв'язувач задіяв парадигму cube-and-conquer (C&C) і спочатку розділяв задачу на мільйон підзадач (cubes). На другій фазі підзадачі розв'язували методом CDCL solver, що також має назву conquer solver.

Розмір файлу з доказами у форматі DRAT  сягнув 200 терабайтів. Із нього було виготовлено й заархівовано сертифікат розміром 68 гігабайтів. Для $7824$ натуральних чисел існує декілька розв'язків проблеми, але для $7825$ розв'язку не знайдено.

У термінології теорії Рамсея автори знайшли дійсне розфарбування для $N=7824$ і довели, що число Радо для рівняння Піфагора у випадку двох кольорів дорівнює $7825$, або стисло: $$R_{2}(a^{2}+b^{2}=c^{2})=7825$$Стаття Марійн Гейле, Олівера Кульмана та Віктора Марека була обрана для доповіді на конференції SAT 2016, що відбулася в Бордо (Франція) в липні 2016 року, та була визнана найкращою роботою.

Висвітлення та обговорення

Марійн Гейле зробив вебсторінку з поясненнями роботи для пересічних відвідувачів і лінками на файли з результатами. На сторінці зібрані десятки посилань на публікації в ЗМІ та фахових виданнях, у тому числі в Nature і Шпіґель, і соціальних мережах. Найзагальнішим постало питання, чи можна суперкомп'ютерні рішення взагалі вважати математикою?

Гейле зі співавторами намагалися знайти особливість знайденого числа $7825$, але його сенс залишився незрозумілим.

Див. також

• Розфарбовування графів
• Теорема Ремзі
• Теорема Шура
• Теорема ван дер Вардена
• Теорема Радо
• Задача здійсненності булевих формул (SAT)