Anthropic публикует полное машинное доказательство Великой теоремы Ферма в Lean 4
Fermat's Last Theorem in Lean 4
Anthropic выложила в открытый доступ полное доказательство Великой теоремы Ферма, проверенное ассистентом Lean 4. Доказательство основано на классическом подходе Фрея, Серра, Рибета, Уайлса и Тейлора-Уайлса и использует библиотеку Mathlib. Проверка проводилась тремя способами: сборка с нуля на Lean 4.33.1, сверка с помощью comparator и независимая проверка ядром nanoda на Rust. Все 60 475 модулей репозитория прошли проверку ядром без аксиом, кроме трёх стандартных. Репозиторий включает 29 511 теорем и 1 450 определений, а также HTML-версию для просмотра в браузере. Проект является исследовательским артефактом и не поддерживается.
Вместе эти проверки устанавливают, что приведённое утверждение следует из трёх аксиом, при условии доверия к ядру Lean (или nanoda) и инструментам проверки.