Самое большое математическое доказательство в мире «весит» 200 ТБ
Проблема Булевых пифагоровых троек решена суперкомпьютером Stampede
Суперкомпьютер Stampede из Техасского университета
Команда ученых объявила о получении решения математической проблемы Булевых пифагоровых троек. Решение получено при помощи суперкомпьютера Stampede Калифорнийского университета. Но его объем составляет 200 ТБ. Это столько, сколько занимали бы оцифрованные материалы Библиотеки Конгресса США. В сжатом состоянии доказательство занимает 68 ГБ. На разворачивание массива полученных данных и верификацию решения понадобится около 30000 часов машинного времени. Если же говорить о проверке решения человеком, но это попросту невозможно — всей жизни не хватит, чтобы выполнить такую работу без помощи компьютера.
Это уже не первое такое решение — сейчас довольно часто математически задачи (особенно в комбинаторике) решаются при помощи мощнейших компьютерных систем, поскольку человек такую работу выполнить попросту не в состоянии. Все бы хорошо, но человек не может проверить правильность решения, слишком большой объем работы. Предыдущий рекорд по объемности решения принадлежал 13 ГБ доказательству, опубликованному в 2014 году. 200 ТБ и вовсе из ряда вон выходящий случай.
Проблема Булевых пифагоровых троек занимала умы математиков многие годы. В 1980 году Рональдом Грэхэмом было предложено даже денежное вознаграждение (целых $100) за решение этой важной задачи. И только сейчас команда специалистов, которая стоит за решением, получила эти средства. А формулировка задачи следующая. Возможно ли окрасить каждое положительное натуральное число в красный или синий цвет, так, чтобы тройка натуральных чисел a, b и c, удовлетворяющих теореме Пифагора a2 + b2 = c2 не была бы окрашена в один и тот же цвет. К примеру, возьмем пифагорову тройку 3,4 и 5. Если 3 и 5 окрашены в синий цвет, то число 4 обязательно должно быть красным.
В статье, опубликованной 3-го мая, ученые доказывают, что до числа 7824 все пифагоровы тройки могут удовлетворять условию задачи. Начиная с числа 7825 это становится уже невозможным. Существует 102300 способов окрасить тройки в разный цвет до числа 7285. Чтобы прийти к такому решению, ученым понадобилось 2 дня машинного времени, с работой 800 процессоров системы Stampede. После этого решение было подтверждено при помощи другой компьютерной программы.
Проблема Пифагоровых троек — одна из многих, относящихся к Теории Рамсея. Это раздел математики, изучающий условия, при которых в произвольно формируемых математических объектах обязан появиться некоторый порядок. Задачи в теории Рамсея обычно звучат в форме вопроса «сколько элементов должно быть в некотором объекте, чтобы гарантированно выполнялось заданное условие или существовала заданная структура».
Несмотря на то, что компьютер решил задачу, он не предоставил ответа на вопрос, почему число 7825 является таким значительным, или почему окрашивание троек в разный цвет вообще возможно. И это извечная проблема машинных доказательств. Они могут быть верными, но математика ли это?
