Проблема Булевых пифагоровых троек решена суперкомпьютером 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 способов окрасить тройки в разный цвет до числа 7825. Чтобы прийти к такому решению, ученым понадобилось 2 дня машинного времени, с работой 800 процессоров системы Stampede. После этого решение было подтверждено при помощи другой компьютерной программы.

Проблема Пифагоровых троек — одна из многих, относящихся к Теории Рамсея. Это раздел математики, изучающий условия, при которых в произвольно формируемых математических объектах обязан появиться некоторый порядок. Задачи в теории Рамсея обычно звучат в форме вопроса «сколько элементов должно быть в некотором объекте, чтобы гарантированно выполнялось заданное условие или существовала заданная структура».

Несмотря на то, что компьютер решил задачу, он не предоставил ответа на вопрос, почему число 7825 является таким значительным, или почему окрашивание троек в разный цвет вообще возможно. И это извечная проблема машинных доказательств. Они могут быть верными, но математика ли это?
Поделиться с друзьями
-->

Комментарии (42)


  1. MELCHIOR1
    27.05.2016 13:48
    +9

    7824 -> 4287 -> 42! Ответ на главный вопрос жизни, вселенной и всего такого
    но что это вычисление троек даёт я так и не понял. Ищется порядок в хаосе?


    1. taujavarob
      27.05.2016 17:21
      +1

      7824 -> 7+8 + 2 + 4 = 21 -> 21*2 = 42

      7824 -> 4287 -> 42* (8-7) = 42*1 = 42


      1. rauch
        27.05.2016 21:54

        21 -> 21*2

        поясните?


        1. Pand5461
          27.05.2016 22:10

          А почему бы и нет?


        1. taujavarob
          27.05.2016 22:20
          +1

          > поясните?

          21 умножаем на 2


          1. rauch
            27.05.2016 22:26

            шутка за триста, спасибо


      1. MnogoBukv
        27.05.2016 23:26

        .del


      1. ximaera
        28.05.2016 00:39

        Профессор Эль Наши, перелогиньтесь!


  1. Imp5
    27.05.2016 13:54
    +4

    Осталось доказать корректность алгоритмов.


    1. Intercross
      06.06.2016 09:39

      Доказательство займёт ещё 300 ТБ и поставит новый рекорд.


  1. APLe
    27.05.2016 14:10
    +7

    По названию статьи было решил, что 200 ТБ занимает составленное компьютером аналитическое доказательство.
    Я правильно понял, что задачу решили просто перебором? «Мы проверили все варианты окраски чисел до 7825 включительно, и выяснили, что ни один из них не удовлетворяет условию»?
    Если так, то новость не очень интересная, хоть объём данных и впечатляет.


    1. dfgwer
      27.05.2016 14:33
      +5

      Там немного по другому.

      «Мы проверили все варианты окраски числе до 7825 включительно, и выяснили, что до 7824 удовлетворяет условию, а 7825 нет»


  1. Murmurianez
    27.05.2016 14:10

    Объем составляет 200 ТБ. В сжатом состоянии доказательство занимает 68 ГБ.
    Неплохо так — на несколько порядков разница.


    1. miksoft
      27.05.2016 14:20
      +1

      Могу предположить, что 200 ТБ — это сильно разреженная матрица. Тогда она действительно будет жаться на много порядков.


      1. Mad__Max
        27.05.2016 21:15
        +1

        У них там 1 миллион матриц (на которые были разбита исходная задача для распараллеливания вычислений), которые очень мало друг от друга отличаются и образуют иерархическую структуру ("дерево") описывающую полное решение.
        Простыми методами архивации они смогли ее ужать "только" до 14 ТБ из исходных 200 ТБ.


        А до 68 ГБ — это они что-то типа программы процедурной генерации написали: как нужно изменить матрицу при каждом ветвлении, чтобы из предыдущий получить следующую и так по цепочке. А после этого еще пожали уже обычными методами архивации (bzip2). В результате чтобы "развернуть" эту иерархическую инкрементную структуру в полный набор данных нужно порядка 13 000 часов процессорного времени. Что всего раза в 3 меньше, чем решить ее заново с нуля.


      1. Moog_Prodigy
        27.05.2016 21:53

        Да, если учесть, что матрица — всего лишь численный результат, а не аналитическое решение- в этом случае увы и ах: ничего особенного тут не достигнуто. А это именно первое.


    1. Lelushak
      28.05.2016 20:00

      Как это несколько порядков? Тут даже один порядок разницы не набирается.


      1. Mad__Max
        29.05.2016 00:53

        Все правильно — несколько порядков. 200 ТераБайт и 68 ГигаБайт. 200 000/68 ~ 2941 раз, больше чем на 3 порядка


  1. korobkinn
    27.05.2016 14:27

    Существует 102300 способов окрасить тройки в разный цвет до числа 7285

    Наверное, все же 7825.


  1. legooleg
    27.05.2016 14:37
    -1

    может, он (суперкомпьютер) просто устал считать и решил сделать число 7824 такой своеобразной границей)


  1. zagayevskiy
    27.05.2016 14:47
    +8

    Несмотря на то, что компьютер решил задачу, он не предоставил ответа на вопрос, почему число 7825 является таким значительным, или почему окрашивание троек в разный цвет вообще возможно. И это извечная проблема машинных доказательств. Они могут быть верными, но математика ли это?

    Бред какой-то. Да, это математика, они предъявили контр-пример. И всё. Ничего особенного они не доказали, они и не пытались. Они всего лишь проверили предположение.


  1. WizAnd
    27.05.2016 14:49
    +2

    Это, конечно, впечатляет, но, в двух словах, какой практический смысл от траты машинного времени в этом вычеслении?


    1. faustxp
      27.05.2016 15:05
      +22

      Так 100$ же.


    1. rusffer
      27.05.2016 15:08
      +2

      Написание научной статьи)


    1. perfect_genius
      06.06.2016 09:41

      Вышивание крестиком?


  1. rrrrex
    27.05.2016 15:08
    +1

    10^2300 И сколько вариантов из этого количества они рассмотрели, чтобы прийти к таким выводам.


    1. ruikarikun
      27.05.2016 15:55

      27825 ~= 102300, то есть это число вариантов при полном переборе.
      Про их алгоритм известно, что они последовательно увеличивали верхнюю грань, так что перебор был на самом деле заметно меньше.


  1. Temych
    27.05.2016 16:06
    +10

    Представим, что этим доказательством решили в России обменяться ученые. И по предлагаемому закону Яровой «о тотальной слежке» эти 200 TB стали одновременно хранить в течение 3 лет все те российские операторы, через которых эта информация прошла.
    Strike!


    1. Kolegg
      28.05.2016 00:17
      +1

      Кстати, было бы забавным сделать эти хранилища сидами для торрентов хранящихся файлов.


      1. Temych
        28.05.2016 00:58

        К сожалению, в таких хранилищах сидами могут быть только товарищи майоры.
        И личами тоже.


    1. SEVENID
      06.06.2016 09:42
      +1

      Секундочку, до меня только сейчас дошло. Это же бесплатное нелимитированное хранилище! Шифруешь и пересылаешь куда угодно то, что нужно сохранить, но негде; когда понадобится или через 2 года — получаешь доступ к собственным данным у оператора и качаешь, из-за чего срок хранения увеличивается ещё на 3 года; повторять, пока не надоест или пока закон не отменят.
      Double strike!


      1. Temych
        06.06.2016 15:01

        Только если договоришься с оператором, что не факт)
        Но вроде сейчас уже будут вносить поправки, что хранить обяжут только метаданные.


  1. saboteur_kiev
    27.05.2016 16:31
    -6

    И ЭТО называют математическим доказательством, а главное принимают решение потратить на это столько ресурсов?
    Всегда считал, что доказательство может быть у теории, а не «любопытной задачки».

    После этого не удивляешься, что правительство вкладывает кучу денег в Маска.
    Там если затраты пока и не окупаются, то хотя бы результат, можно пощупать и попользоваться.


    1. mx2
      06.06.2016 09:39

      Доказательство может быть у чего угодно, в том числе у теоремы Пифагора, которая на теорию никак не тянет.
      Гуманитарии всё переврали, в статье речь не о доказательстве, а о проверке гипотезы. К доказательству это имеет слабое отношение.


  1. tmin10
    27.05.2016 17:50
    -2

    Если же говорить о проверке решения человеком, но это попросту невозможно — всей жизни не хватит, чтобы выполнить такую работу без помощи компьютера.
    Так зачем проверять руками? Нужно просто тоже написать программу, которая перепроверит все данные. Можно даже брать случайные примеры и проверять их.


  1. beliakov
    27.05.2016 22:35
    +1

    Возможно ли окрасить каждое положительное натуральное число в красный или синий цвет...

    Натуральными называют числа, возникающие при естественном счете предметов — 1, 2, 3… Иногда к натуральным числам относят ноль. Отрицательные числа не являются натуральными, поэтому уточнение «положительные» здесь излишне.

    Это ошибка перевода. Смотрим первоисточник:

    The problem asks whether it is possible to colour each positive integer either red or blue...

    «integer» переводится как «целое».


  1. xut
    28.05.2016 09:18

    Число ходов в шахматах 10^118, они могли перебрать все шахматные партии!


  1. Mixim333
    28.05.2016 15:47

    Эта задача воистину пример так модной сейчас «Big Data» — при таких объемах реально начинаешь понимать, что такое «оптимизация» и как она важна, хоть и использовался Метод «грубой силы».


  1. Bakra
    06.06.2016 09:31

    Если же говорить о проверке решения человеком, но это попросту невозможно — всей жизни не хватит, чтобы выполнить такую работу без помощи компьютера.

    У них даже четверка из примера никак не закрашена на картинке, пусть перепроверяют свои алгоритмы. Можете не благодарить.


  1. azsx
    06.06.2016 09:39

    > И ЭТО называют математическим доказательством, а главное принимают решение потратить на это столько ресурсов?
    это называется вычислительным доказательством, а вы хотите аналитического доказательства. В мире «розовых пони» можно аналитическому уму Шерлока Холмса и ожидать от математиков кратких теорем и формул, которые логичны и верны. В реальном мире бывает сложно вывести доказательство аналитически. Проще посчитать все возможные варианты.
    То есть вы можете проверить вычислительный алгоритм на любом другом компьютере и убедится в том, что цифра 7824 это ответ на всё. Поэтому его называют вычислительным доказательством.


  1. dolbanutik
    06.06.2016 09:55

    Думаю не лишним было бы указать, что данный раздел математики непосредственно предполагает что доказательства или решение задач следует получать именно перебором данных. Из той же Вики о теории Рамсея:
    Для результатов в рамках теории Рамсея характерны два свойства. Во-первых, они неконструктивны. Доказывается, что некоторая структура существует, но не предлагается никакого способа её построения кроме прямого перебора. Во-вторых, чтобы искомые структуры существовали, требуется, чтобы объекты, их содержащие, состояли из очень большого числа элементов. Зависимость числа элементов объекта от размера структуры, как минимум, экспоненциальная.
    То есть ставить вопрос о том, математика ли это — некорректно. Это именно тот раздел математики, который предполагает решения такими методами.


  1. OFFREAL
    06.06.2016 10:02

    Но на картинке не все положительные натуральные числа окрашены в красный или синий цвет! Как это понимать?