Содержание
Claude формализовал доказательство Великой теоремы Ферма: Anthropic получила машинно проверяемую версию на 13 млн строк кода. Компания утверждает, что ее внутренняя исследовательская модель справилась за 11 дней, хотя математики оценивали такую работу в годы.
Речь идет не о новом доказательстве теоремы. Claude переложил уже известную математическую конструкцию в язык, который проверяет компьютер. Для математики это почти как портировать огромный старый проект на строгий компилятор, где каждая лемма должна собраться без ошибок.
Доказательство Уайлса перевели на язык Lean
Великая теорема Ферма появилась в 1637 году, когда Пьер де Ферма записал свою знаменитую гипотезу. Полное доказательство дал Эндрю Уайлс только в 1995 году. Его работа заняла 129 страниц и закрыла задачу, которая прожила больше трех с половиной веков.
Формализация работает иначе, чем обычная публикация в журнале. Математик пишет рассуждение для людей, а система Lean требует каждую зависимость, каждый переход и каждое утверждение. Если где-то осталась дырка, проверка не проходит.
Lean давно используют в математике для таких задач. Это специализированный язык и proof assistant, где теоремы превращают в код. Компьютер затем проверяет, что вывод следует из аксиом и уже доказанных утверждений.
По данным Anthropic, агенты Claude по ходу работы доказали около 30 300 отдельных теорем. В финальную версию вошли примерно 29 500 из них.
- Объем: 13 млн строк кода Lean
- Срок работы: 11 дней непрерывного запуска
- Доказанные теоремы: около 30 300
- Использовано в финале: около 29 500 теорем
- Человеческая помощь: редкие подсказки высокого уровня
13 млн строк — больше, чем основная библиотека Mathlib
Масштаб здесь легко недооценить. Anthropic заявляет, что итоговое доказательство больше Mathlib более чем в пять раз. Mathlib — основная библиотека сообщества Lean, на которую опираются многие формальные проекты.
Это похоже на ситуацию, где нейросеть не просто дописала пару модулей. Она собрала отдельный массив математической инфраструктуры. В него вошли алгебра, гармонический анализ, геометрия и теория чисел.
Математик Кевин Баззард из Imperial College London назвал результат «чрезвычайным достижением автоформализации». По его словам, доказательство использует только аксиомы математики и показывает, что артефакты ИИ уже достаточно надежны для дальнейшей работы.
Есть и трезвая часть истории. Anthropic добилась результата не с первой попытки. Предыдущие запуски внесли около 7% финальных строк без учета шаблонного кода. То есть 11 дней — это срок успешного прогона, а не вся история экспериментов.
ИИ в математике ускоряется, но работа все еще тяжелая
Anthropic связывает успех не только с моделью Claude. Компания дала агентам доступ к открытому инструменту Prove2Me, который создали внешние разработчики. Он помогает выбирать следующий полезный шаг в длинной цепочке доказательства и снижает расходы на инференс.
Месяцем ранее Anthropic рассказывала о другом результате, связанном с дзета-функцией Римана. Эта функция стоит в центре гипотезы Римана, одной из самых известных нерешенных задач математики.
OpenAI тоже идет в эту сторону. Лаборатория использует модель Astra для работы над классическими задачами Эрдеша. Тот же проект, по данным компании, сузил несколько старых открытых вопросов в теоретической информатике.
Для читателя из мира железа тут понятная аналогия. Когда компилятор собирает 13 млн строк без ошибок, это не доказывает красоту архитектуры. Зато он беспощадно проверяет формальные связи. В математике такая проверка убирает человеческое «ну тут очевидно».
Anthropic расширила бесплатный доступ и исследовательские кредиты для математиков, которые занимаются формализацией. Компания также готовит более крупные гранты под такие проекты. Даже с Claude финальная машинная запись Великой теоремы Ферма заняла 11 дней непрерывной работы.
«Along the way we see autoformalization of algebra, harmonic analysis, geometry and number theory», — сказал Кевин Баззард, описывая многослойность получившегося доказательства.
