Компьютер частично разрешил математическую проблему, выдав доказательство более чем на 15 тысяч страниц — перепроверить его вручную невозможно. Это поднимает вопрос об исключении человека из математики, пишет (перевод из их статьи самого главного).
Если в школе разбор доказательств к теоремам и так казался пыткой, то теперь представьте, что вам пришлось столкнуться с доказательством размером с Википедию. Исследователи компьютерных технологий из университета Ливерпуля — Алексей Лисица и Борис Конев — получили математическое доказательство, которое изложено в 13-гигабайтом файле, превышающим все сложенные вместе страницы Википедии. Ручная проверка доказательства не представляется возможной.
Тем не менее, это большой шаг вперед в решении проблемы несоответствия, которая была предложена знаменитым венгерским математиком Палом Эрдешем в 1930-е. характеризует структуру подпоследовательности также, как и всю бесконечную последовательность.
Основная гипотеза Эрдеша состояла в том, что может быть найдено несоответствие любой величины, но он так никогда не смог этого доказать. Ученые решили воспользоваться компьютером, чтобы доказать, что бесконечная последовательность всегда будет иметь несоответствие, равное двум или большему числу. Компьютер потратил на проверку шесть часов и выдал доказательство длиннее Огромной Теоремы, изложенной на 15000 листах.
Проверить этот массив данных для человека не представляется возможным, и если доказательство с расхождением 2 оказалось настолько сложным, значит ручной проверке не пригодны и доказательства с большими расхождениями. Это поднимает вопрос о математике, из которой исключен человек: если доказательство может быть проверено только на компьютере, может ли оно считаться верным? По мнению Джила Калаи из Института математики в еврейском университете в Иерусалиме, исключительно человеческого мозга здесь недостаточно. Но если другой компьютер получит такое же доказательство с теми же результатами, тогда его можно считать верным.
Лисица и Конев уже приступили к следующему проекту — их компьютер остаются включенным на протяжении недель, чтобы найти результат отклонения со значением три.
Подробнее узнать о недоступном для человеческого ума доказательстве проблемы несоответствия можно на сайте Verge.
Тем не менее, это большой шаг вперед в решении проблемы несоответствия, которая была предложена знаменитым венгерским математиком Палом Эрдешем в 1930-е. характеризует структуру подпоследовательности также, как и всю бесконечную последовательность.
Основная гипотеза Эрдеша состояла в том, что может быть найдено несоответствие любой величины, но он так никогда не смог этого доказать. Ученые решили воспользоваться компьютером, чтобы доказать, что бесконечная последовательность всегда будет иметь несоответствие, равное двум или большему числу. Компьютер потратил на проверку шесть часов и выдал доказательство длиннее Огромной Теоремы, изложенной на 15000 листах.
Проверить этот массив данных для человека не представляется возможным, и если доказательство с расхождением 2 оказалось настолько сложным, значит ручной проверке не пригодны и доказательства с большими расхождениями. Это поднимает вопрос о математике, из которой исключен человек: если доказательство может быть проверено только на компьютере, может ли оно считаться верным? По мнению Джила Калаи из Института математики в еврейском университете в Иерусалиме, исключительно человеческого мозга здесь недостаточно. Но если другой компьютер получит такое же доказательство с теми же результатами, тогда его можно считать верным.
Лисица и Конев уже приступили к следующему проекту — их компьютер остаются включенным на протяжении недель, чтобы найти результат отклонения со значением три.
Подробнее узнать о недоступном для человеческого ума доказательстве проблемы несоответствия можно на сайте Verge.