Один из самых сложных и прославленных математических результатов XX века — последняя теорема Ферма — впервые была переведена на язык компьютерного кода. Этот прорыв осуществил усовершенствованный чат-бот Клод от компании Anthropic. Разработчики сообщили, что их ИИ-модель справилась с задачей всего за 11 дней. Для сравнения: по оценкам специалистов, у команды математиков на аналогичную работу ушло бы около десяти лет.
Суть открытия, которое доказал еще в 1994 году Эндрю Уайлз, проста для формулировки, но дьявольски трудна для подтверждения: для любого числа n больше 2 не найдется таких целых чисел, чтобы выполнялось равенство x² + y² + n² = z² + n². Однако практическая ценность этого достижения не в самом уравнении, а в методах, которые родились в ходе его доказательства. Они позволили сблизить далекие друг от друга разделы математики.
Математическое сообщество поражено. Профессор Алекс Конторович из Ратгерского университета признался, что способность машины превратить работу человека в 13 миллионов строк неопровержимого кода потрясла его до глубины души. Дэниел Литт из Университета Торонто отметил, что если ИИ подчинилась теорема Ферма, то, вероятно, ей под силу формализовать что угодно.
Нюанс в том, что сгенерированный Клодом массив данных пока нельзя сразу интегрировать в общую библиотеку MathLib, используемую математиками. Однако сам факт автоматической проверки знакового доказательства снял последние сомнения в его безупречности. Кевин Баззард из Имперского колледжа Лондона, который лично возглавляет проект по формализации теоремы Ферма (рассчитанный на десять лет), заявил: если раньше он был на 99,9% уверен в правоте Уайлза, то теперь его уверенность достигла 100%.
Эксперты считают, что ИИ ждет роль строгого, но быстрого рецензента. В современной науке, где объем публикаций растет, а качество проверки падает, появление «волшебной палочки», которая мгновенно находит ошибки в работах с arXiv, стало бы спасением для исследователей. Однако есть и обратная сторона: если каждый начнет создавать собственные библиотеки кода, научное сообщество рискует потеряться в хаосе несовместимых файлов.
Ранее физики смогли устранить давнюю математическую проблему в одной из ключевых теорем квантовой теории информации — обобщенной квантовой лемме Штайна.