Клод завершил первое компьютерное доказательство последней теоремы Ферма

Компания Anthropic сообщила, что ее модель Claude предоставила первое полное компьютерное доказательство последней теоремы Ферма за 11 дней, написав доказательство на языке программирования Lean.

Компания сообщила, что Клод работал в основном автономно, сгенерировал 13 миллионов строк бережливого кода и доказал 30 300 теорем, из которых 29 500 были использованы в окончательном доказательстве.

Последняя теорема Ферма гласит, что никакие натуральные числа a, b и c не удовлетворяют aⁿ + bⁿ = cⁿ для любого числа n, большего 2. Теорема оставалась недоказанной более 350 лет, пока Эндрю Уайлс не опубликовал первое общепринятое доказательство в 1995 году.

Исследователь-антрополог Тяньи Пэн начал проект, чтобы проверить, сможет ли Клод добиться прогресса в формализации теоремы. Ожидалось, что работа по формализации займет годы, и математическое сообщество использовало 86-страничный план на начальном этапе работы.

Доказательство Клода следует упрощенной версии доказательства Уайлса от Дармона, Даймонда и Тейлора. Антропик сказал, что человеческий вклад был ограничен случайными инструкциями высокого уровня от Пенга, включая такие подсказки, как "Якобиан как схема имеет высокий приоритет" и "необходимо как можно скорее завершить разработку теоремы Мазура".

Кевин Баззард из Имперского колледжа Лондона, который в 2024 году запустил проект по формализации теоремы в Lean, назвал результат "выдающимся достижением в области автоформализации". Он сказал, что работа продемонстрировала автоформализацию в алгебре, гармоническом анализе, геометрии и теории чисел.

По словам Антропика, первые попытки Клода провалились из-за того, что агенты потеряли представление о состоянии проекта и перестали эффективно сотрудничать. На эти неудачные попытки пришлось около 7% нестандартных строк в окончательном доказательстве.

Компания заявила, что ее усилия увенчались успехом после перехода на Prove2Me, открытую платформу для совместной работы по формализации математики, разработанную Пенгом и его коллегами из Колумбийского университета. С помощью Prove2Me и мультиагентной системы на основе кода Claude доказательство было завершено чуть менее чем за две недели с использованием около шести миллиардов выходных токенов из внутренней исследовательской модели, примерно сравнимой с Claude Fable 5.1.

Anthropic сказал, что Lean проверил готовое доказательство, используя свои три стандартные аксиомы, и компаратор подтвердил, что утверждение теоремы соответствует утверждению последней теоремы Ферма в Mathlib. Компания заявила, что объем доказательства более чем в пять раз превышает объем Mathlib, основной библиотеки математических доказательств сообщества, на которой основана теорема.

Баззард сказал, что автоматическая формализация последней теоремы Ферма станет "большим шагом на пути к автоматической формализации современной математической литературы". Он сказал, что такие методы могут помочь найти ошибки в существующих математических работах и снизить нагрузку на судей.

Антропик также сообщил, что исследователи, используя три личных плана Клода Макса, формализовали теорему Виноградова о трех простых числах за три дня с помощью Prove2Me. Компания сообщила, что расширила поддержку внешних исследователей с помощью бесплатных подписок и скидок, исследовательских кредитов и грантов для более крупных научных проектов.

Featured image credit

>