Секретный проект по разрешению спорного математического доказательства с помощью компьютера.

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

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

Сага началась в 2012 году, когда Синъити Мочизуки из Киотского университета в Японии заявил, что доказал известную идею, называемую гипотезой ABC, опубликовав в интернете доказательство на 500 страницах. Гипотеза проста в формулировке и касается простых чисел, входящих в решения уравнения a + b = c, и того, как эти числа связаны друг с другом. Но для её решения требуется глубокое понимание природы взаимодействия сложения и умножения. Ответ также имеет далеко идущие последствия для других математических дисциплин.

Доказательство Мочизуки стало настоящей математической сенсацией, но многим его коллегам было трудно его понять, поскольку оно включало в себя новые методы и концепции, которые он в совокупности назвал межуниверсальной теорией Тейхмюллера (IUT). В последующие месяцы видные математики пытались прояснить работу Мочизуки, в том числе в беседах с самим Мочизуки, но вопрос о правильности доказательства зашёл в тупик.

В 2018 году, после того как два видных математика — Петер Шольце из Боннского университета и Якоб Стикс из Франкфуртского университета имени Гёте (оба из Германии) — объявили об обнаружении возможной ошибки, дальнейшего прогресса не наблюдалось. Мочизуки и группа его близких коллег, в основном из Киотского университета, утверждали, что доказательство верно, в то время как большая часть математического сообщества заявляла, что доказательство в лучшем случае не поддается расшифровке, а в худшем — содержит фатальные ошибки.

Однако в прошлом году Мочизуки протянул руку примирения своим скептикам и предложил потенциальный путь вперед. Был достигнут огромный прогресс в области математики, называемой формализацией, где письменные математические доказательства переводятся на компьютерный язык, способный автоматически проверять их корректность. Один из таких языков, Lean, больше всего привлек Мочизуки. В то время он писал: «[Lean] — это лучшая и, возможно, единственная технология… для достижения значимого прогресса в отношении фундаментальной цели — освобождения математической истины от ига социальных и политических динамик».

Источник: www.newscientist.com