Anthropic заявила, что Claude завершил первое полное формализованное доказательство великой теоремы Ферма. Это не повторное открытие теоремы, а переписывание существующего доказательства в виде логического кода, который компьютер может проверить построчно. Компания сообщила, что на эту работу ушло 11 дней, в результате чего было сгенерировано около 13 миллионов строк.
Значение формализованного доказательства заключается в том, чтобы записать математические рассуждения на языке, доступном для проверки машиной. Традиционные доказательства в научных статьях часто требуют длительной проверки коллегами, и если где-то в цепочке обнаруживается ошибка, процесс её исправления может длиться месяцы или даже годы. Великая теорема Ферма была доказана британским математиком Эндрю Уайлсом в 1995 году, но перевод всего этого доказательства в полностью машинно-проверяемую форму долгое время считался чрезвычайно сложным инженерным проектом.
Достижение долгосрочной цели проекта за 11 дней
Математик Лондонского имперского колледжа Кевин Баджард с 2024 года продвигает соответствующий проект, цель которого — переписать доказательство Уайлса в помощнике доказательств Lean. Согласно первоначальному плану, эта работа требует длительного сотрудничества, и финансирование обеспечено до 2029 года.
Anthropic заявила, что Claude опередил другие аналогичные цели в выполнении этой задачи. После проверки Buzzard отметил, что это доказательство может быть подтверждено без дополнительных предположений, то есть исключительно на основе базовых аксиом математики.
Выполняется параллельно несколькими агентами
Согласно информации от Anthropic, команда исследователей из Колумбийского университета под руководством Тяньи Пэн заставила несколько агентов Claude работать параллельно, каждый из которых отвечал за написание определений и доказательств более мелких утверждений, а затем постепенно объединял их в более крупные доказательственные структуры. Человеческое вмешательство было минимальным и заключалось главным образом в задании приоритетов на каждом этапе.
Первоначальный прогресс шел не гладко. Anthropic сообщила, что некоторые агенты временно не могли делиться завершенным контентом и дублировали работу. Затем команда использовала инструмент Prove2Me, чтобы предоставить всем агентам единый список задач и способ организации файлов, а также сохранить заметки на естественном языке, помогая им повторно использовать результаты друг друга.
- Более 30 000 поддерживающих теорем
- Общий расход достиг нескольких миллиардов токенов
- В итоге подтверждено около 13 миллионов строк
Важно не новая теорема, а проверяемость
Основной акцент этого достижения не на открытии новых математических утверждений, а на преобразовании уже существующих важных доказательств в версии, которые могут быть пошагово проверены компьютером. По мере роста числа математических статей и контента, сгенерированного ИИ, стоимость ручной проверки доказательств построчно также возрастает, что делает формальные инструменты все более актуальными.
Anthropic также отметила, что объем этого доказательства превышает в пять раз размеры общедоступной библиотеки Mathlib, используемой математическим сообществом. Полный файл уже загружен на GitHub, и исследователи могут продолжить построчную проверку его структуры и корректности.