Доказательство последней теоремы Ферма впервые целиком формализовали на языке Lean — теперь компьютер может проверить каждый шаг логической цепочки. Команда ИИ-агентов Claude за 11 дней подготовила около 13 млн строк кода и 29,5 тыс. промежуточных теорем.

Речь не о новом доказательстве самой теоремы. Формализация следует аргументу Эндрю Уайлса и Ричарда Тейлора, опубликованному в 1995 году. Новизна в том, что пропущенные в обычном математическом изложении переходы сделали явными и проверяемыми программой.

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

Формализация не делает доказательство удобнее для чтения и не добавляет нового математического результата. Её значение в другом: обширные доказательства можно переводить в машинно проверяемую форму значительно быстрее, что в перспективе способно облегчить поиск ошибок и рецензирование новых работ.

Фото: Anthropic.