Claude переписал теорему Ферма
Следите за новостями по этой теме!
Подписаться на «Рифы и пачки / Твоя культура»
Компания Anthropic заявила, что ее система искусственного интеллекта Claude создала полностью проверяемую компьютером версию доказательства Великой теоремы Ферма — одной из самых известных задач в истории математики.
Гипотезу сформулировал французский математик Пьер де Ферма в 1637 году. Она утверждает, что для целых положительных чисел уравнение xⁿ + yⁿ = zⁿ не имеет решений при n больше 2. Полное доказательство опубликовал британский математик Эндрю Уайлс в 1995 году; обычная математическая версия занимала 129 страниц.
Anthropic не открывала теорему заново. Компания перевела уже существующее доказательство в формальный вид — то есть записала математические рассуждения как код, который специальная программа способна проверять автоматически, шаг за шагом и без доверия к человеческой интуиции.
По первоначальным оценкам, такая работа должна была занять несколько лет. Однако внутренней исследовательской версии Claude, по словам Anthropic, потребовалось 11 дней непрерывной и в основном автономной работы. Люди давали системе общие указания, но не занимались постоянным ручным написанием кода.
Итоговый результат состоит примерно из 13 миллионов строк специализированного кода на языке Lean, который используют математики для формализации доказательств. Это более чем в пять раз больше, чем Mathlib — главная общественная библиотека формальных математических доказательств.
В процессе агенты Claude, как сообщается, доказали около 30 300 отдельных теорем, а в финальную версию включили примерно 29 500 из них. Эти промежуточные результаты охватывали алгебру, гармонический анализ, геометрию и теорию чисел. Несколько предыдущих неудачных попыток также внесли вклад: на них пришлось около 7% строк итогового текста, не относящихся к стандартному шаблонному коду.
Математик Кевин Баззард из Имперского колледжа Лондона назвал достижение выдающимся. По его оценке, система доказала Великую теорему Ферма, опираясь только на аксиомы математики, а созданные формальные конструкции уже достаточно надежны, чтобы служить основой для дальнейшей работы.
Новый результат появился примерно через месяц после сообщения Anthropic о другом проекте, связанном с дзета-функцией Римана. Эта функция занимает центральное место в гипотезе Римана — одной из самых трудных нерешенных задач современной математики.
Похожее направление развивает и OpenAI: лаборатория использует модель Astra для решения классических задач, связанных с именем математика Пала Эрдёша. Сообщалось, что эта работа также помогла сузить несколько давних открытых вопросов теоретической информатики.
По словам Anthropic, решающую роль сыграл доступ Claude к открытому программному инструменту Prove2Me, созданному внешними сотрудниками. Он помогает ИИ выбирать следующий полезный шаг в длинном исследовательском процессе и одновременно снижает вычислительные расходы на работу модели.
Anthropic расширила бесплатный доступ и исследовательские кредиты для математиков, занимающихся формализацией доказательств, а также предложила отдельные крупные гранты. Но радоваться полной победе машин над математиками пока рано: даже при столь высокой скорости формализация одной большой теоремы потребовала 11 дней и 13 миллионов строк кода. Человечеству, похоже, пока не отменили работу — лишь добавили к ней очень говорливого цифрового стажера.
PEREC.RU
Anthropic сообщила о формализации Великой теоремы Ферма с помощью внутренней версии ИИ Claude. Формализация означает перевод обычного математического доказательства в программный код, который система Lean может проверять автоматически по отдельным шагам. Это не новое доказательство теоремы, а компьютерная реконструкция уже известной работы британского математика Эндрю Уайлса, опубликовавшего полное доказательство в 1995 году.
Великую теорему Ферма сформулировал французский математик Пьер де Ферма в 1637 году. Она утверждает, что уравнение xⁿ + yⁿ = zⁿ не имеет решений в положительных целых числах, если показатель степени n больше 2. Доказательство Уайлса в обычной математической записи занимало 129 страниц.
Anthropic ожидала, что перевод доказательства в формальный код займет несколько лет. По заявлению компании, Claude выполнил основную работу за 11 дней непрерывной, в основном автономной работы. Человеческое участие ограничивалось общими рекомендациями, без постоянного ручного написания кода.
Финальная версия содержит около 13 миллионов строк кода на языке Lean. Это более чем в пять раз превышает размер Mathlib — главной общественной библиотеки формальных математических доказательств. В ходе проекта агенты Claude доказали приблизительно 30 300 отдельных теорем, а около 29 500 из них вошли в окончательную версию. Использовались результаты из алгебры, гармонического анализа, геометрии и теории чисел. Прежние попытки формализации также внесли вклад: на них пришлось примерно 7% нестандартных строк финального кода.
Математик Кевин Баззард из Имперского колледжа Лондона назвал результат выдающимся и отметил, что доказательство опирается только на математические аксиомы. Он также заявил, что полученные формальные конструкции достаточно надежны для дальнейшего использования.
Проект стал частью более широкой гонки ИИ-лабораторий за автоматизацию математических исследований. Примерно за месяц до этого Anthropic рассказывала о работе с дзета-функцией Римана, связанной с гипотезой Римана — одной из самых известных нерешенных задач. OpenAI использует модель Astra для изучения классических задач Пала Эрдёша и, по сообщениям, сузила ряд открытых вопросов теоретической информатики.
Anthropic связывает успех с доступом Claude к открытому инструменту Prove2Me, созданному внешними сотрудниками. Программа помогает ИИ выбирать наиболее полезный следующий шаг в многоэтапной работе и снижает вычислительные расходы. Компания также расширила бесплатный доступ, исследовательские кредиты и грантовую поддержку для математиков, занимающихся формализацией.
Главный вывод двойственен. ИИ заметно ускоряет перевод сложных доказательств в машинно проверяемый вид, но сама процедура остается трудоемкой. Одиннадцать дней — рекордно быстро по первоначальным оценкам, однако результат все равно измеряется 13 миллионами строк специализированного кода.
