Спорный математический довод — тот, который делит поле уже более десяти лет — может быть наконец решен неожиданным судьей: компьютерной программой. Сердце спора вращается вокруг попытки Синити Мочизуки 2012 года решить гипотезу ABC, давно существующую проблему, глубоко уходящую корнями в фундаментальную природу чисел.
Гипотеза ABC сосредоточена на предельно простом уравнении, включающем три целых числа: a + b = c. Она предполагает конкретные правила, регламентирующие то, как простые числа, составляющие эти целые числа, должны быть связаны друг с другом. Решение этой кажущейся элементарной проблемы могло бы открыть глубокие познания в области математики, потенциально повлияв на другие знаменитые гипотезы, такие как последняя теорема Ферма.
Мочизуки, профессор Кётоского университета в Японии, представил свой довод в рамках сложной конструкции, созданной им самим, под названием интер-универсальная теория Тейхмюллера (IUT). Однако, чрезмерная техничность и непонятная для большинства математиков природа теории IUT сделала ее в значительной степени нечитаемой для тех, кто пытался проверить его работу. Изначальный энтузиазм сменился разочарованием, поскольку эксперты боролись с ее замысловатыми нюансами.
Добавляя масла в огонь, в 2018 году два видных немецких математика — Петер Шольц и Якоб Стикс — выявили потенциальный изъян в доказательстве Мочизуки. Мочизуки парировал их аргумент, и в отсутствие всеобъемлющего органа для разрешения математических споров поле расслоилось на два лагеря: те, кто в основном принимал общепринятую точку зрения (поддерживаемую большинством математиков), и меньшая группа,aligned с Мочизуки и его институтом в Кёто.
Теперь Мочизуки предлагает путь вперед через формализацию — преобразование своего доказательства из человекочитаемого математического обозначения в Lean, язык программирования, специально разработанный для строгой математической верификации. Этот процесс потенциально позволил бы компьютерам автоматически проверять согласованность его аргументов, предлагая беспрецедентный уровень объективности.
Мочизуки считает, что Lean обладает уникальными возможностями для преодоления сложных языковых и концептуальных барьеров, которые остановили прогресс в понимании теории IUT. Он рассматривает ее как инструмент для освобождения математической истины от потенциальных предвзятостей, присущих человеческому толкованию.
Хотя некоторые эксперты, такие как Кевин Будзард из Imperial College London, видят в этом перспективное направление, они также признают колоссальный вызов, который стоит перед ним. Формализация теории IUT потребовала бы перевода огромных масс сложных уравнений на синтаксис Lean — предприятия, сравнимого с одними из самых масштабных проектов формализации, когда-либо предпринимаемых. Такие усилия часто вовлекают целые команды математиков и программистов, занимающие месяцы или даже годы.
Йохан Коммелин из Утрехтского университета в Нидерландах, хотя и осторожно оптимистично настроен, подчеркивает, что успех зависит от неизменной преданности Мочизуки делу. Он предостерегает, что если проект будет преждевременно заброшен, это может стать лишь очередным эпизодом затянувшейся саги, отмеченной неразрешенными спорами.
Даже в случае успеха, — отмечает Коммелин, — даже при компьютерной проверке кода, разногласия по поводу толкования могут сохраниться. Lean может разрешить логические противоречия, но не обязательно погасить все философские или концептуальные разногласия, касающиеся работы Мочизуки.
В конечном счете, хотя формализация предлагает проблеск надежды на разрешение этого вечного математического противостояния, остается открытым вопрос, сможет ли она преодолеть глубоко укоренившиеся сложности и различные точки зрения, которые характеризовали дебаты о доказательстве гипотезы ABC.
