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

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

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

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

Проблема

Річард Радо^[en]

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

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

N = 1344 , 1514 {\displaystyle N=1344,1514}

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

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

R 2 ( a 2 + b 2 = c 2 ) > 6500 {\displaystyle R_{2}(a^{2}+b^{2}=c^{2})>6500}

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

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

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

N = 7664 {\displaystyle N=7664}

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

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

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

Теорема

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

Доведення

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

…

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

Розмір файлу з доказами у форматі DRAT ^{[К 3]} сягнув 200 терабайтів. Із нього було виготовлено й заархівовано сертифікат розміром 68 гігабайтів. Для ${\displaystyle 7824}$ натуральних чисел існує декілька розв'язків проблеми, але для ${\displaystyle 7825}$ розв'язку не знайдено^[12][13].

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

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

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

Гейле зі співавторами намагалися знайти особливість знайденого числа ${\displaystyle 7825}$, але його сенс залишився незрозумілим^[17].

Див. також

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

Коментарі

1. Розфарбовування чисел множини ${\displaystyle \{1,2,3,...,N\}}$ (для деякого ${\displaystyle N}$) називається дійсним, якщо воно не має монохроматичних розв'язків цього рівняння. Трійка чисел ${\displaystyle \{a,b,c\}}$ називається монохроматичною в разі ідентичності значень функції розфарбування для кожного елемента: ${\displaystyle \chi (a)=\chi (b)=\chi (c)}$.
2. CDCL — скорочення від Conflict-Driven Clause Learning^[en] — кероване конфліктами навчання диз'юнктам
3. DRAT — скорочення від англ. Deletion Resolution Asymmetric Tautology

Примітки

1. Erdős, P.; Graham, R.L. (1980). Old and New Problems and Results in Combinatorial Number Theory (PDF). Université de Genève. Процитовано 10 листопада 2016.
2. Soifer, Alexander (2009). The Mathematical Coloring Book. Mathematics of Coloring and the Colorful Life of Its Creators. New York: Springer-Verlag. с. xxvii. doi:10.1007/978-0-387-74642-5. ISBN 978-0-387-74640-1. Процитовано 11 листопада 2016.
3. Shreevatsa, R (20 травня 2016). A simple-to-state problem has been resolved, and there's surprisingly little about this in the news. WordPress.com. Процитовано 10 листопада 2016.
4. Lamb, Evelyn (26 травня 2016). Two-hundred-terabyte maths proof is largest ever. Nature. Процитовано 31 серпня 2016. (укр. 200 терабайт «математики»)
5. Croot, Ernie; Lev, Vsevolod F. (2007). Open Problems in Additive Combinatorics (PDF): 14 (proposed by Graham). Процитовано 10 листопада 2016.
6. Graham, Ron (2008). Old and New Problems and Results in Ramsey Theory (PDF). University of California, San Diego: 6. Процитовано 10 листопада 2016.
7. Cooper, Joshua Cooper; Poirel, Chris (4 грудня 2008). Note on the Pythagorean Triple System (PDF). University of South Carolina, Virginia Tech. Процитовано 10 листопада 2016.
8. Cooper, Joshua; Poirel, Chris (February 18, 2013 (Submitted on 20 Sep 2008)). Pythagorean Partition-Regularity and Ordered Triple Systems with the Sum Property. ArXiv.org. Процитовано 10 листопада 2016.
9. Kay, William (2012). An Overview of the Constructive Local Lemma. Ann Arbor: University of South Carolina. ISBN 9781267319937. Архів оригіналу за 12 листопада 2016. Процитовано 10 листопада 2016.
10. Myers, Kellen John (May, 2015). Computational Advances In Rado Numbers. New Brunswick, New Jersey: Rutgers, The State University of New Jersey. Процитовано 11 листопада 2016.
11. Joshua Cooper, Ralph Overstreet (2015). Coloring so that no Pythagorean Triple is Monochromatic. ArXiv.org.
12. Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek (2016). Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer. ArXiv.org. doi:10.1007/978-3-319-40970-2_15.
13. Everything's Bigger in Texas. University of Texas at Austin. 2016. Процитовано 31 серпня 2016.
14. Heule, Marijn J. H.; Oliver Kullmann, Victor W. Marek (11 червня 2016). Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer (PDF). Theory and Applications of Satisfiability Testing – SAT 2016 (вид. Volume 9710 of the series Lecture Notes in Computer Science). Springer. с. 228—245. doi:10.1007/978-3-319-40970-2_15. Процитовано 31 серпня 2016. {{cite conference}}: Cite має пусті невідомі параметри: |розташування= та |авторлінк= (довідка)
15. 19th International Conference on Theory and Applications of Satisfiability Testing. SAT 2016. July 5-8, 2016. Процитовано 31 серпня 2016.
16. Dambeck, Holger (30.05.2016). Der längste Mathe-Beweis der Welt. Der Spiegel. Процитовано 10 листопада 2016.
17. Lipton, RJ; Regan, KW (4 вересня 2016). How Hard, Really, is SAT?. Gödel's Lost Letter and P=NP. Процитовано 10 листопада 2016.