Уже более десяти лет математическое сообщество ведет ожесточенные споры о подлинности одного масштабного и крайне спорного доказательства. Сегодня на передний план выходит новая технологическая область — компьютерная формализация, которая предлагает потенциальный способ наконец разрешить этот спор.
Конфликт вокруг гипотезы ABC
В центре конфликта находится гипотеза ABC — фундаментальная проблема, касающаяся взаимосвязи между сложением и умножением простых чисел. В 2012 году Синъити Мотидзуки из Киотского университета опубликовал 500-страничное доказательство, претендующее на решение этой давней загадки.
Однако его метод — сложнейшая теоретическая база, называемая межуниверсальной теорией Тейхмюллера (IUT), — оказался настолько беспрецедентным, что разделил мировое математическое сообщество. В то время как Мотидзуки и его сторонники настаивают на правильности доказательства, многие выдающиеся математики, включая Питера Шольце и Якоба Стикса, утверждают, что в логике содержится фатальная ошибка.
Этот тупик создал редкое для современной науки состояние «патовой ситуации»: одна сторона видит в работе прорывную истину, в то время как другая — неразборчивые или ошибочные рассуждения.
Расцвет формализации
Чтобы выйти из этого замкнутого круга, исследователи обращаются к Lean — специализированному языку программирования, предназначенному для «формализации». В этом процессе математические доказательства переводятся в код, который компьютер может проверить с абсолютной логической достоверностью. Это исключает «человеческий фактор» — возможность недопонимания, социального давления или предвзятости при рецензировании — и заменяет его бинарной истиной.
В настоящее время два разных проекта пытаются использовать эту технологию, чтобы поставить точку в этом вопросе:
1. Проект LANA (Поиск истины)
Под руководством Фумихару Като из математического центра ZEN, проект «Lean and Anabelian geometry» (LANA) стремится верифицировать доказательство раз и навсегда. В эту группу входят эксперты как по специфическим теориям Мотидзуки, так и по языку программирования Lean.
Несмотря на достигнутый прогресс, проект столкнулся с серьезным препятствием. Они выявили в теории IUT конкретный проблемный момент, который зеркально отражает ошибку, обнаруженную Шольце и Стиксом в 2018 году. После восемнадцати месяцев интенсивного изучения команда всё еще не может распутать этот логический узел.
2. Проект Мотидзуки (Поиск ясности)
Используя иной подход, Мотидзуки и его коллеги также начали формализовать свою работу на языке Lean. Однако их цель — не «доказать» собственную правоту (так как они считают её уже установленной), а использовать код как инструмент точной коммуникации.
Мотидзуки утверждает, что Lean создаст «точную запись» его логической структуры, что сделает её неуязвимой для неверных интерпретаций, которые годами подпитывали полемику. Хотя его команда уже создала первые 70 строк кода, эксперты отмечают, что это лишь самое начало колоссальной работы.
Почему это важно
Разрешение вопроса с гипотезой ABC — это не просто вопрос одного уравнения; это поворотный момент в самой практике математики.
- Кризис верификации: Если компьютер обнаружит ошибку, это положит конец десятилетию академических трений.
- Новая методология: Если доказательство подтвердится, это докажет, что «формализация» является жизнеспособным способом работы с математическими идеями, сложность которых превышает когнитивные пределы человека.
- Мост для коммуникации: Диалог между проектом LANA и группой Мотидзуки показывает, что технологии могут наконец предоставить общий язык математикам, которые иначе не способны эффективно общаться друг с другом.
Заключение
Несмотря на огромные технические трудности, переход к математике, проверяемой компьютерами, представляет собой первое реальное движение в споре вокруг гипотезы ABC за многие годы. Подтвердит ли код работу Мотидзуки или исправит её, результат фундаментально изменит способы установления и передачи математической истины.
