Max Home IndustryИдея о том, что компьютеры играют ключевую роль в математическом доказательстве, сегодня хорошо воспринимается всеми, кроме чистосердечных математиков, но последний пример компьютерного доказательства выходит в новую сферу — доказательство размером 200 терабайт.
Проблема троек Пифагора является или была открытой проблемой в теории Рамсея:
Можно ли разделить набор натуральных чисел 1,2,3 … на две части так, чтобы ни одна часть не содержала троек Пифагора, то есть трех чисел, которые образуют стороны прямоугольного треугольника и где:
а2 + Ь2 = с2.
Вы также можете представить проблему, пытаясь раскрасить пифагоровы тройки двумя цветами, чтобы ни одна тройка не была одного цвета.
Существует также связанная с этим проблема, которая спрашивает, можно ли тройки разделить на k наборов или раскрасить в n цветов. Проблема с двумя наборами является самой простой, и ее нужно решить в первую очередь.
Это одна из тех замечательных математических задач, которые легко сформулировать, но очень, очень сложно решить. Вы можете начать достаточно легко, и когда вы соберете первую тройку — хорошо известную тройку треугольников 3,4,5, вы можете просто положить тройку в один сет, а 4 и 5 — в другой. Вы можете продолжать так, но 5 также входит в другую тройку 5,12,13, поэтому теперь вы не можете поместить 12 и 13 в тот же набор, что и 5, но 12 и 13 являются частью еще двух троек 12,35, 37 и 13,84,85. Вы можете видеть, что по мере вашего продвижения ограничения на то, как распределяются номера, становятся все труднее и труднее.
Вопрос в том, можно ли это сделать?
Приз ждал ответа двадцать лет, и теперь мы знаем, что ответ отрицательный, но доказательство само по себе примечательно.
В принципе, все, что вам нужно сделать, это найти встречный пример, но, как вы можете видеть из небольшого примера, это становится все труднее, когда вы добавляете все больше и больше чисел. До недавнего времени лучшим результатом было то, что набор {1,2,3 ,,, 7664} может быть разбит на разделы, поэтому, если вы собираетесь найти встречный пример, вы должны смотреть за пределы 7664 — 7825, скажем.
Как указано в документе, объявляющем результат, вы можете проверить, что n = 7824 имеет раздел, удовлетворяющий условию, за несколько секунд — просто покажите раздел и проверьте, нет ли троек ни в одной из частей. С другой стороны, чтобы доказать, что n = 7825 не имеет такого разбиения, нужно рассмотреть все возможные разбиения.
Суперкомпьютер Stampede в Техасском вычислительном центре — 270 терабайт (ТБ) RAM, 14 петабайт (ПБ) дискового пространства и 522080 процессорных ядер.
Время для компьютерных поисков. При использовании решателя SAT можно рассмотреть возможность изучения всех возможностей, но, по оценкам, на это потребуется 35 000 процессорных часов. Для решения этой задачи был использован суперкомпьютер, кластер Stampede в Техасском центре передовых вычислений, имеющий 800 ядер, для поиска решения примерно за два дня.
Решатель SAT обычно просто выдает ответ «да» или «нет» на вопрос «может ли эта формула выполняться?», Но недавно была проделана работа, чтобы заставить их предоставить формальные доказательства результата. Окончательное «доказательство» было размером 200 терабайт, которое можно было сжать до 68 гигабайт.
Ясно, что это доказательство не читается человеком.
Итак, теперь мы знаем, что тройная проблема Пифагора с k = 2 разрешима для n <7825, но невозможна для больших n. Есть ли более короткие, удобочитаемые и, возможно, понятные доказательства? Обратите внимание, что существует огромное доказательство асимметрии того, что существует разбиение, удовлетворяющее условию, и доказательство того, что его нет. Чтобы доказать, что все, что вам нужно сделать, это дать разбиение и позволить кому-нибудь проверить, нет ли пифагоровой тройки ни в одном из множеств. Чтобы доказать, что такого раздела нет, вы должны рассмотреть все разделы и показать, что все они выходят из строя. Если бы было более короткое математическое доказательство, тогда должна была бы быть логическая структура, которая инкапсулирует очевидную сложность перечисления неудовлетворительных разделов. Это то же самое, что, скажем, простая формула для числа пи, но нет такой формулы для большинства иррациональных чисел - и это, по сути, мера информации Колмогорова. Необязательно, чтобы доказательство было значительно короче, чем полное перечисление того, что оно доказывает. Предполагается, что такой подход можно использовать для решения других комбинаторных задач, поэтому, возможно, математикам нужно привыкнуть к идее, что «доказательство» может означать терабайты данных.