Материал подготовлен автоматически по первоисточникам: ссылки на них — в конце статьи.
Anthropic сообщила: Claude завершил первую формализацию доказательства Великой теоремы Ферма в Lean. Это не новое доказательство, а перевод уже известного математического рассуждения в код, который может проверить ассистент доказательств. Результат показывает, что ИИ способен участвовать в формализациях, на которые эксперты отводили годы.
Теорему доказал Эндрю Уайлс в 1995 году. Claude не предложил другой путь к результату, а представил существующее доказательство в форме, где Lean последовательно проверяет каждый логический переход.
Формализация превысила 13 млн строк и стала крупнейшим доказательством на Lean. Основной объём создала не только сама теорема: для неё потребовалось доказать более 29 тыс. вспомогательных теорем из областей математики, которые прежде не были формализованы. Такой масштаб показывает, что узким местом становится и наполнение библиотеки проверенных знаний.
Для команд, которые рассматривают ИИ и Lean для критически важной логики, это аргумент в пользу схемы, где модель пишет формальное доказательство, а Lean проверяет результат. Это не аргумент в пользу доверия обычному ответу модели без проверяющего слоя. Пост не раскрывает долю ручной работы, поэтому по нему нельзя оценить автономность и стоимость такого процесса.
Источники
Похоже на вашу задачу?
Расскажите, что собираете. За полчаса разложим на этапы и назовём сроки — это бесплатно и ни к чему не обязывает.
