Более десятилетия математики не могут прийти к единому мнению о том, является ли доказательство в 500 страниц верным. Теперь перевод доказательства в компьютерную форму может окончательно решить этот вопрос.
Компьютеры могут проверять математические доказательства monsitj/Getty Images
Один из самых противоречивых споров в математике может быть решен с помощью компьютера, что потенциально положит конец ожесточенному спору о сложном доказательстве, который длится уже более десятилетия.
Проблемы начались в 2012 году, когда Синъити Мотидзуки из Киотского университета в Японии ошеломил математический мир обширным 500-страничным доказательством ABC-гипотезы – важной нерешённой проблемы, затрагивающей самую суть существования чисел. Доказательство использовало высокотехнологичную и абстрактную концепцию, разработанную Мотидзуки, – так называемую межуниверсальную теорию Тейхмюллера (IUT), – которая казалась непостижимой даже большинству опытных математиков, пытавшихся её понять.
ABC-гипотеза, которой уже более 40 лет, основана на, казалось бы, простом уравнении трёх целых чисел a + b = c и определяет, как должны соотноситься друг с другом простые числа, составляющие эти числа. Помимо глубокого понимания фундаментальной природы взаимодействия сложения и умножения, эта гипотеза имеет значение для других известных математических гипотез, таких как Великая теорема Ферма.
Эти потенциальные последствия поначалу воодушевили математиков на проверку доказательства, но первые усилия зашли в тупик, и Мотидзуки сетовал на то, что не было предпринято дальнейших усилий для осмысления работы. Затем, в 2018 году, два видных немецких математика, Петер Шольце из Боннского университета и Якоб Стикс из Франкфуртского университета имени Гёте, объявили, что нашли возможную брешь в прочности доказательства.
Но Мотидзуки отверг их аргументы, и, поскольку не было высшего судебного органа, который мог бы вынести решение о том, кто прав, а кто нет, обоснованность теории IUT разделилась на два лагеря: с одной стороны, большая часть математического сообщества, с другой — небольшая группа исследователей, слабо связанных с Мотидзуки и Научно-исследовательским институтом математических наук в Киото, где он является профессором.
Теперь Мотидзуки предложил возможный выход из тупика. Он предложил перевести доказательство из его нынешней формы, в математической нотации, предназначенной для людей, на язык программирования Lean, который мог бы автоматически проверяться и верифицироваться компьютером.
Этот процесс, называемый формализацией, — непрерывная область исследований, которая может полностью изменить подход к математике. Формализация доказательства Мотидзуки предлагалась и раньше, но он впервые выразил желание продолжить этот проект.
Мотидзуки не ответил на просьбу прокомментировать эту статью, но в недавнем отчете он утверждал, что Lean хорошо подойдет для разрешения разногласий между математиками, которые препятствуют широкому принятию его доказательства: «[Lean] — лучшая и, возможно, единственная технология… для достижения значимого прогресса в отношении фундаментальной цели освобождения математической истины от ига социальной и политической динамики», — пишет Мотидзуки.
По словам Мотидзуки, он убедился в достоинствах формализации после посещения недавней конференции по Lean в Токио в июле, в частности, после того, как увидел ее способность обрабатывать те виды математических структур, которые, по его словам, необходимы для его теории IUT.
Это потенциально перспективное направление для выхода из тупика, считает Кевин Баззард из Имперского колледжа Лондона. «Если это написано на языке бережливого производства, то это не безумие, верно? Многое в газетах написано на очень странном языке, но если это можно записать на языке бережливого производства, то это значит, что, по крайней мере, этот странный язык стал совершенно чётко определённым», — говорит он.
«Мы хотим понять, почему [существует IUT], и ждали этого более 10 лет», — говорит Йохан Коммелин из Утрехтского университета в Нидерландах. «Lean поможет нам найти ответы на эти вопросы».
Однако и Баззард, и Коммелин утверждают, что формализация теории IUT станет гигантской задачей и потребует перевода огромного количества математических уравнений, которые в настоящее время существуют только в понятной для человека форме. Этот проект будет сопоставим с некоторыми из крупнейших когда-либо реализованных проектов формализации, которые часто требуют участия команд опытных математиков и специалистов по бережливому производству, занимая месяцы или годы.
Эта пугающая перспектива может оказаться непривлекательной для небольшой горстки математиков, квалифицированных для участия в этом проекте. «Людям придётся серьёзно подумать, готовы ли они тратить много времени на работу над проектом, который в конечном итоге может обернуться провалом», — говорит Баззард.
Но даже если математикам удастся завершить проект, а код Lean покажет, что теорема Мотидзуки не содержит противоречий, математики, включая самого Мотидзуки, все равно могут спорить о ее значении, говорит Коммелин.
«Lean может оказать большое влияние и положить конец спорам, но только если Мотидзуки действительно будет придерживаться своего нового решения формализовать свою работу», — говорит он. «Если он уйдёт через четыре месяца, сказав: „Ладно, я попробовал, но Lean слишком глуп, чтобы понять моё доказательство“, то это будет просто новая глава в очень длинной череде глав, где мы всё ещё застряли на социальной проблеме».
И, несмотря на весь оптимизм, который Мотидзуки проявляет по отношению к Lean, он также соглашается со своими критиками в том, что толкование смысла кода может привести к дальнейшим разногласиям, написав, что Lean «в настоящее время, судя по всему, не представляет собой какого-либо “волшебного лекарства” для полного решения социальных и политических проблем».
Однако Баззард надеется, что успешная формализация, по крайней мере, сможет сдвинуть с места десятилетнюю сагу, особенно если Мотидзуки добьётся успеха. «С программным обеспечением не поспоришь», — говорит он.
Источник: www.newscientist.com
