Великая теорема Ферма утверждает, что уравнение xⁿ + yⁿ = zⁿ не имеет решений в натуральных числах при n больше 2. Пьер Ферма набросал её на полях в 1630-х; Эндрю Уайлс доказал её в 1990-х с помощью одной из самых трудных математик, когда-либо написанных. 4 сентября 2026 года Anthropic объявила, что Claude за 11 дней создал первую полную проверенную компьютером версию этого доказательства[1]. В статье объясняется, что это значит, почему это история не только о математике, но и об информатике, и чего это не означает.
Хронология
- 1630-еФерма заявляет о доказательстве, для которого «эти поля слишком узки».
- 1994–95Эндрю Уайлс (вместе с Ричардом Тейлором) завершает доказательство.
- 2024Кевин Баззард начинает в Имперском колледже Лондона человеческий проект формализации доказательства в Lean.
- авг. 2026Агенты Claude за 11 дней завершают полную формализацию в Lean.
- 4 сент. 2026Anthropic объявляет результат; Баззард его просматривает.
Что делает система доказательства
Базовый уровень GCSE
Доказательство, написанное человеком, оставляет мелкие шаги читателю. Даже опытные рецензенты могут пропустить пробел. Система интерактивного доказательства вроде Lean устраняет этот риск. Определения и доказательства пишутся как код, а небольшой доверенный проверщик (ядро) подтверждает, что каждый шаг следует из логики и ранее доказанного. Если код компилируется, теорема проверена. Это как компилятор, который отказывается запускать программу, пока не доказано, что она верна.
Формальное доказательство — это дерево: итоговая теорема опирается на крупные промежуточные результаты, те — на леммы, а леммы — на определения и базовые факты. Lean проверяет каждую связь. Нажмите кнопку, чтобы проверить дерево от основания. Схема; настоящее дерево содержит около 29 500 теорем.
Что на самом деле сделал Claude
Углублённый уровень A-Level
- Он формализовал упрощённый вариант доказательства Уайлса, предложенный Дармоном, Даймондом и Тейлором[1].
- Результат — около 13 миллионов строк на Lean и около 30 300 теорем (примерно 29 500 использованы в итоговом доказательстве), более чем в пять раз больше Mathlib[1].
- Десятки агентов Claude работали параллельно 11 дней, использовав около шести миллиардов выходных токенов внутренней исследовательской модели[1].
- Математический вклад людей ограничился эпизодическими общими указаниями исследователя Anthropic Тяньи Пэна[1].
- Доказательство опирается только на три стандартные аксиомы Lean, а сравнительный инструмент подтвердил, что итоговая теорема утверждает ровно то же, что и формулировка Великой теоремы Ферма в самой Mathlib[1].
- В нём повторно использованы части проекта FLT Кевина Баззарда в Имперском колледже Лондона, и Баззард просмотрел готовое доказательство[1].
Быстрая проверка
Что означает, что доказательство «компилируется» в Lean?
Почему важно проверить формулировку
Проверенное компьютером доказательство полезно, только если оно доказывает нужное утверждение. Если бы теорема была слегка неверно записана в Lean, идеальное доказательство не того ничего бы не стоило. Поэтому команда с помощью сравнительного инструмента подтвердила, что формулировка совпадает с независимо написанной версией в Mathlib, и поэтому важна проверка «никаких лишних аксиом»: она показывает, что ничего не было просто принято на веру[1]. Верификация шагов и валидация спецификации — две разные задачи, точно как в тестировании программ.
Различие, которое учащиеся часто упускают
Верное — не значит изящное (или новое).
Вопрос в формате экзамена
Объясните разницу между верификацией и валидацией на примере формального доказательства Великой теоремы Ферма. [4 баллов]
Показать образец ответа и разбивку баллов
- верификация проверяет, что продукт сделан правильно, то есть соответствует спецификации (1 балл)
- здесь Lean проверяет, что каждый шаг доказательства логически верен (1 балл)
- валидация проверяет, что сделан нужный продукт, то есть спецификация соответствует тому, что действительно требовалось (1 балл)
- здесь сравнение формулировки в Lean с независимой формулировкой FLT в Mathlib проверяет, что доказана именно та теорема, которая имелась в виду (1 балл)
На что обращает внимание экзаменатор: определить оба термина и привязать каждый к конкретной части примера.
Частая ошибка: считать эти слова синонимами. Программа может пройти все проверки верификации и всё равно делать не то.
Логика, доказательства и тестирование связывают математику и информатику A-Level. Статья Умеет ли ИИ по-настоящему решать математику? показывает общую картину, а задачи тысячелетия — какие вопросы ещё открыты.
Источники и дополнительное чтение
- Anthropic: Formalizing Fermat's Last Theorem (4 Sep 2026) — масштаб, агенты, аксиомы, вклад людей, рецензия Баззарда, оговорки
- AI Weekly: Claude formalized Fermat's Last Theorem in 11 days — новостное освещение
- Lean community: Mathlib — математическая библиотека Lean
- Imperial College London: Fermat's Last Theorem formalisation project (Kevin Buzzard) — проект под руководством людей
Последняя проверка: 5 октября 2026 г. Цифры являются типичными опубликованными значениями, и правила могут изменяться. Формулировки в экзаменах различаются в зависимости от спецификации — проверьте свою.
Часто задаваемые вопросы
Это ИИ доказал Великую теорему Ферма?
Нет: её доказал Эндрю Уайлс в 1990-х. В 2026 году агенты Claude перевели вариант этого доказательства на Lean — язык программирования, проверщик которого контролирует каждый логический шаг. Результат, объявленный Anthropic 4 сентября 2026 года, — первое полное доказательство теоремы, проверенное компьютером.
Что такое Lean?
Система интерактивного доказательства: язык программирования, на котором определения, теоремы и доказательства записываются как код. Небольшая доверенная программа — ядро — проверяет, что каждый шаг следует из правил логики и ранее доказанного. Если доказательство компилируется, теорема проверена при допущении лишь встроенных в Lean аксиом.
Насколько велико доказательство?
Около 13 миллионов строк кода на Lean и около 30 000 теорем (примерно 29 500 использованы в итоговом доказательстве) — более чем в пять раз больше Mathlib, главной математической библиотеки сообщества Lean. Работа заняла 11 дней: десятки агентов Claude трудились параллельно при эпизодических общих указаниях исследователя Anthropic Тяньи Пэна.
Хорошее ли это доказательство, написанное ИИ?
Оно верно в том смысле, что Lean его проверил, и Кевин Баззард, руководящий человеческим проектом формализации FLT в Имперском колледже Лондона, его просмотрел. Но Anthropic говорит, что оно, вероятно, гораздо длиннее необходимого, а неудачные попытки оставили около 7 % его содержательных строк. Верное и изящное — разные вещи.
Оценки и отзывы читателей
Оцените эту статью по нескольким критериям — ваше мнение помогает другим читателям и помогает нам становиться лучше.
Была ли эта статья полезной?
Расскажите, что вы думаете — исправление, вопрос, оставшийся без ответа, или тема, которую вы хотели бы увидеть далее.
Хотите обсудить голосом? Запишитесь на бесплатный видеозвонок в удобное время: 15 минут для короткого вопроса, 30 — для всего остального. Время показывается в вашем часовом поясе.
Об авторе
Sudershan Soni
Основатель и главный преподаватель в Mostak Services — репетитор по математике, естественным наукам, информатике и STEM со степенью магистра и более чем 20-летним профессиональным опытом, преподаёт ученикам от уровня 11+ и GCSE до A-Level и выше, онлайн по всему миру.
Читать полный профиль