Claude впервые формализовал Великую теорему Ферма в Lean. Почему это не «решил», а «записал»

Привет, друзья. У меня немного странные ощущения от этой новости. С одной стороны — да, впервые в истории программа самостоятельно превратила одну из самых знаменитых математических теорем в код, который можно проверить построчно. С другой — и тут важно не дёргаться от заголовков — саму теорему никто заново не доказал. Поэтому прежде чем радоваться или пугаться, давайте аккуратно разложим, что именно произошло.

Что именно сделал Claude

Великая теорема Ферма — та самая, которую в XVII веке Пьер Ферма записал на полях «Арифметики» Диофанта с припиской «я нашёл этому изумительное доказательство, но поля слишком узки, чтобы его вместить». Доказал её только в 1995 году Эндрю Уайлс, использовав работы Фрея, Серра, Рибета и Тейлора–Уайлса. Это доказательство — на десятки страниц, и оно никогда не было записано на языке, который компьютер может проверить сам.

4 сентября 2026 года Anthropic опубликовала: Claude за 11 дней написал 13 миллионов строк на Lean 4 — это язык для машинной проверки доказательств. Из них 30 300 теорем были доказаны в процессе, и 29 500 вошли в итоговое доказательство. Доказательство использует только три стандартные аксиомы Lean и не требует никаких дополнительных допущений.

Дальше важное: Anthropic не проверяла результат сама. Код скачал математик Кевин Баззард из Imperial College London — он уже несколько лет ведёт собственный многолетний проект по той же формализации, рассчитанный до 2029 года. Баззард скомпилировал репозиторий и подтвердил: proof is sorry-free — на жаргоне Lean это значит «нет заглушек, нет недоказанных мест, всё доказано до самого верха». Его цитата: «Это выдающееся достижение автоформализации. Теорема Ферма доказана без каких-либо допущений, кроме аксиом математики».

Почему именно проверка Баззарда — это важная часть новости: иначе вся история превратилась бы в пресс-релиз компании о собственных успехах. А так — независимый рецензент с репутацией, который изначально должен был сделать то же самое руками, посмотрел и сказал «да, оно работает».

Что формализация НЕ означает

Здесь стоит остановиться, потому что вчерашние пересказы в соцсетях разделились на два противоположных лагеря. Одни пишут «Claude решил теорему Ферма!» — это неверно. Другие, наоборот, отмахиваются: «ну это же просто переписать текст в код» — это тоже неверно.

Представьте себе огромное доказательство на сотнях страниц. Каждый шаг опирается на предыдущий. Любая ошибка, опечатка, скрытое допущение — и вся конструкция рушится. Когда люди читают такое доказательство глазами, они неизбежно пропускают какие-то места, особенно в самых скучных леммах. Формализация — это перевод каждого шага на формальный язык, где каждое утверждение обязано быть либо доказанным, либо выкинутым. Lean — такой «безжалостный репетитор по математике»: он не пропустит ни одну строку.

Но — и это критично — Lean проверяет уже существующее доказательство Уайлса. Он не придумывает новый аргумент. Задача, которую решил Claude, глубже, чем кажется: нужно не просто «переписать», а понять, какой именно путь от A к B использует доказательство, и заполнить этим формальные дыры, которых в математической статье никто не видит. В Lean-проекте Buzzard’а, например, только черновик первой фазы формализации — это 86 страниц инструкций, написанные вручную. Claude прошёл по ним и написал сам код.

Почему 11 дней — это серьёзно

Если вы думаете «ну и что, компьютер же быстрый» — посмотрите на цифры по-другому. Тот же Lean-проект, который ведёт Buzzard, по плану рассчитан до 2029 года — это ручная работа целой команды профессиональных математиков с экспертизой в формальных методах. Anthropic сделал похожую по объёму работу за полторы недели с помощью языковой модели, которая в основном работала автономно, под небольшим человеческим контролем. Под «автономно» Anthropic имеет в виду: модель сама решала, какие подзадачи закрывать, какие аксиомы использовать, какие инструменты вызывать.

Платформа, на которой это крутилось, называется Prove2Me — её разработала команда исследователя Tianyi Peng из Columbia University. Это не «волшебный запрос к чату», а многоагентная система, где агенты на разных ролях (скажем, один пишет код, другой проверяет, третий ищет контрпример) координируются между собой. Прошлым летом та же команда уже показывала похожий результат — Claude за полтора дня улучшил доказательство по гипотезе Римана с 41,6% до 67,2% подтверждённого покрытия. Уайлс бы такое не оценил, но тот же вектор — машины становятся полезными там, где раньше были только люди с карандашом.

Что это меняет на практике

Мне кажется, эта новость — не про математику. Она про три вещи, которые выходят за рамки теоремы Ферма.

Во-первых, проверка кода. Индустрия ПО давно страдает от того, что баги прячутся в «очевидных» кусках кода. Если модели могут формально доказывать корректность доказательств — логично, что в обозримом будущем они смогут и доказывать корректность программ. Это не замена тестированию, а его усиление.

Во-вторых, это удар по многолетним академическим проектам. Стиль работы «десять лет командой пишем проверки» перестанет быть оправданным. Anthropic уже показала, что сжатие срока с лет до дней — это не магия, а инженерия.

В-третьих, и это самое тонкое — это меняет отношение к ошибкам. Сейчас многие большие доказательства в математике существуют как «текст + доверие». После Lean-формализации это заменяется на «текст + проверяемый машинный код». Сообщество пока сопротивляется этой смене, но, по-моему, лет через десять без формализации публикация просто не пройдёт рецензирование в серьёзных журналах.

Где у меня остаются вопросы

Я честно не знаю, насколько обобщаем этот результат. Lean-формализация FLT — это большая, но конкретная задача: есть готовое доказательство Уайлса, есть многолетний roadmap от Buzzard’а, есть хорошо проработанная библиотека Mathlib. То есть Claude шёл по относительно ровному маршруту. Что будет, когда поставишь ему задачу вроде «формализуй доказательство гипотезы Римана» — где готового текста нет и где формализация сама по себе требует изобретения новой математики? Это уже совсем другой уровень сложности, и я не вижу оснований думать, что он поддастся так же легко.

Второй вопрос — про надёжность Lean-ядра. Buzzard написал: доказательство опирается только на три стандартные аксиомы. Это правда, и это плюс. Но сам Lean — программа. У неё есть версии, баги, обновления. До 2026 года в ядре Lean уже находили серьёзные ошибки (знаменитый инцидент в 2023 году с аксомой propext, который потом быстро исправили, но всё же). Это значит, что формальное доказательство — это не абсолютная истина, а истина относительно конкретной версии ядра. Для математики, которая живёт тысячелетиями, это даже немного некомфортно.

Резюме

4 сентября 2026 года — это не «Claude решил Ферма», это «Claude за 11 дней сделал работу, которую человек-планировал делать до 2029 года, и сделал её корректно». Большая разница. Это значимо, но не сенсация — это инженерная веха, а не открытие нового континента.

Но если посмотреть шире — направление движения ясно. Машины учатся брать на себя не просто текст и картинки, а логические конструкции, которые ещё недавно считались прерогативой человека с карандашом и долгими годами сосредоточенной работы. Мне как айтишной девочке немного не по себе от того, как быстро это происходит. Но и немного восторженно — потому что это тот случай, когда AI не заменяет человека, а берёт на себя самую скучную часть работы, оставляя человеку самое интересное: понять, что вообще считать истиной.

Хорошего вам вечера и не теряйте любопытства. 🐾