Проблема трійок Буля — Піфагора
Проблема трійок Буля — Піфагора полягає у відповіді на питання, чи можна поділити множину натуральних чисел на дві частини так, щоб у кожній частині не було жодної піфагорової трійки. Марійн Гейле[en], Олівер Кульман та Віктор Марек[en] 2016 року довели, що це можливо лише для і менших чисел. Для множини з чисел і більше такий поділ неможливий. Іншими словами, серед натуральних чисел , розфарбованих у два кольори, завжди знайдеться монохроматична трійка , і що .
У стислій формі результат записується через число Радо для рівняння Піфагора: .
Проблема трійок Буля — Піфагора виникла в теорії Ремзі, головним мотивом якої є заперечення абсолютного хаосу в достатньо великих системах[1][2]. Проблема стосується питання, чи можна поділити множину натуральних чисел на дві частини так, щоб кожна частина не мала жодної піфагорової трійки, тобто таких , і що . У термінах фарбування чисел проблема виглядає так: чи можна розфарбувати натуральні числа у два кольори щоби жодна піфагорова трійка не була монохроматичною. Основні роботи теорії Ремзі, що пов'язані з проблемою трійок Буля — Піфагора, включають теореми Шура[en], ван дер Вардена та Радо[en][3].
У 1980-х Рональд Грем запропонував приз у розмірі 100 доларів тому, хто розв'яже цю проблему [4]. У 2007—2008 роках він нагадав, що проблема була сформульована ще в його публікації разом із Палом Ердешем 1980 року[1], зазначив про обмаль даних, щоб вирішити проблему в той чи інший спосіб, і за Ердешевою традицією пообіцяв премію (250 дол.) за результат[5][6].
У грудні 2008 року Джошуа Купер і Кріс Пойрел надрукували перший приклад розподілу множини натуральних чисел на дві частини так, що кожна частина не мала жодної піфагорової трійки. На обчислення пішло сотні годин процесорного часу. Результат було представлено у вигляді панелі чорних і білих квадратиків. Квадратик із координатами () задавав колір числа . Числа збільшувались знизу до гори, потім зліва направо[7][8].
2012 року Вільям Кей застосував алгоритм[en] Робіна Мосера та Габора Тардоса[en] та знайшов розв'язок проблеми трійок для множини [9].
У травні 2015 року Келлен Маєрс і Дорон Зілбергер оприлюднили роботу зі втілення алгоритму здійсненності булевих формул (SAT) для обчислення чисел Радо, зокрема, для проблеми трійок Буля — Піфагора. Вони запровадили поняття дійсного розфарбовування[К 1], яке дає можливість знайти нижню межу для числа Радо. У результаті комп'ютерних обчислювань Маєрс і Зілбергер знайшли, що число Радо , та опублікували сертифікат існування дійсного розфарбовування множини у трьох формах:
- Рядок довжиною з елементів для позначення кольору всіх чисел у послідовності.
- Два списки чисел, що показує, у яку з двох частин потрапило кожне число під час розбивки.
- Панель червоних і синіх квадратиків, в якій нумерація квадратиків збільшується зліва направо, потім зверху донизу[10].
У наведеній нижче візуалізаційній панелі червоний колір замінено на жовтий.
У травні 2015 року Джошуа Купер і Ральф Оверстріт розфарбували двома кольорами натуральних чисел так, що всі піфагорові трійки були різнокольоровими [11].
Марійн Гейле, Олівер Кульман та Віктор Марек у травні 2016 року вирішили проблему трійок Буля — Піфагора за допомогою теореми 1.
Теорема 1. Множину натуральних чисел можна поділити на дві частини так, щоб кожна частина не мала жодної піфагорової трійки, але це не можливо для .
Доведенням першого твердження теореми став позитивний приклад розфарбування двома кольорами натуральних чисел. Приклад проілюстровано панеллю квадратиків трьох класів: двох пофарбованих і нефарбованого. До нефарбованого класу належать числа, що не входять до жодної піфагорової трійки, та деякі числа з трійок, чий колір не має значення. Нижній рядок у панелі займають числа , над ним — і так далі до верхнього рядка .
… | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Науковці провели попередній аналіз усіх варіантів розфарбування чисел та зменшили обсяг доведення другого твердження теореми до близько трильйона () здебільшого досить складних варіантів. Теорема була доведена шляхом перебору всіх знайдених варіантів, використовуючи розв'язувач класу SAT Solver на 800 ядерному суперкомп'ютері Stampede у Комп’ютерному центрі Техаського університету[en] протягом двох днів. Розв'язувач задіяв парадигму cube-and-conquer (C&C) і спочатку розділяв задачу на мільйон підзадач (cubes). На другій фазі підзадачі розв'язували методом CDCL solver[К 2], що також має назву conquer solver.
Розмір файлу з доказами у форматі DRAT [К 3] сягнув 200 терабайтів. Із нього було виготовлено й заархівовано сертифікат розміром 68 гігабайтів. Для натуральних чисел існує декілька розв'язків проблеми, але для розв'язку не знайдено[12][13].
У термінології теорії Рамсея автори знайшли дійсне розфарбування для і довели, що число Радо для рівняння Піфагора у випадку двох кольорів дорівнює , або стисло: Стаття Марійн Гейле, Олівера Кульмана та Віктора Марека була обрана для доповіді на конференції SAT 2016, що відбулася в Бордо (Франція) в липні 2016 року, та була визнана найкращою роботою[14][15].
Марійн Гейле зробив вебсторінку з поясненнями роботи для пересічних відвідувачів і лінками на файли з результатами[13]. На сторінці зібрані десятки посилань на публікації в ЗМІ та фахових виданнях, у тому числі в Nature[4] і Шпіґель[16], і соціальних мережах. Найзагальнішим постало питання, чи можна суперкомп'ютерні рішення взагалі вважати математикою?
Гейле зі співавторами намагалися знайти особливість знайденого числа , але його сенс залишився незрозумілим[17].
- Розфарбовування графів
- Теорема Ремзі
- Теорема Шура[en]
- Теорема ван дер Вардена
- Теорема Радо[en]
- Задача здійсненності булевих формул (SAT)
- ↑ Розфарбовування чисел множини (для деякого ) називається дійсним, якщо воно не має монохроматичних розв'язків цього рівняння. Трійка чисел називається монохроматичною в разі ідентичності значень функції розфарбування для кожного елемента: .
- ↑ CDCL — скорочення від Conflict-Driven Clause Learning[en] — кероване конфліктами навчання диз'юнктам
- ↑ DRAT — скорочення від англ. Deletion Resolution Asymmetric Tautology
- ↑ а б Erdős, P.; Graham, R.L. (1980). Old and New Problems and Results in Combinatorial Number Theory (PDF). Université de Genève. Процитовано 10 листопада 2016.
- ↑ 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.
- ↑ 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.
- ↑ а б Lamb, Evelyn (26 травня 2016). Two-hundred-terabyte maths proof is largest ever. Nature. Процитовано 31 серпня 2016. (укр. 200 терабайт «математики»)
- ↑ Croot, Ernie; Lev, Vsevolod F. (2007). Open Problems in Additive Combinatorics (PDF): 14 (proposed by Graham). Процитовано 10 листопада 2016.
- ↑ Graham, Ron (2008). Old and New Problems and Results in Ramsey Theory (PDF). University of California, San Diego: 6. Процитовано 10 листопада 2016.
- ↑ Cooper, Joshua Cooper; Poirel, Chris (4 грудня 2008). Note on the Pythagorean Triple System (PDF). University of South Carolina, Virginia Tech. Процитовано 10 листопада 2016.
- ↑ 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.
- ↑ Kay, William (2012). An Overview of the Constructive Local Lemma. Ann Arbor: University of South Carolina. ISBN 9781267319937. Архів оригіналу за 12 листопада 2016. Процитовано 10 листопада 2016.
- ↑ Myers, Kellen John (May, 2015). Computational Advances In Rado Numbers. New Brunswick, New Jersey: Rutgers, The State University of New Jersey. Процитовано 11 листопада 2016.
- ↑ Joshua Cooper, Ralph Overstreet (2015). Coloring so that no Pythagorean Triple is Monochromatic. ArXiv.org.
- ↑ 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.
- ↑ а б Everything's Bigger in Texas. University of Texas at Austin. 2016. Процитовано 31 серпня 2016.
- ↑ 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 має пусті невідомі параметри:|розташування=
та|авторлінк=
(довідка) - ↑ 19th International Conference on Theory and Applications of Satisfiability Testing. SAT 2016. July 5-8, 2016. Процитовано 31 серпня 2016.
- ↑ Dambeck, Holger (30.05.2016). Der längste Mathe-Beweis der Welt. Der Spiegel. Процитовано 10 листопада 2016.
- ↑ Lipton, RJ; Regan, KW (4 вересня 2016). How Hard, Really, is SAT?. Gödel's Lost Letter and P=NP. Процитовано 10 листопада 2016.