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) и инструментам проверки.
- black_knight
Интересно, есть ли какие-то части кода на Lean, которые можно было бы передать в существующие библиотеки Lean.
Мой опыт показывает, что требуется много ручного труда, чтобы заставить Fable писать код достаточно хорошего качества для библиотеки формализации, с которой могли бы работать другие. Но поскольку здесь, безусловно, формализовано и много предварительных результатов, было бы хорошо, если бы не все усилия были потрачены впустую на одно главное доказательство!
(Повтор более раннего комментария, но, думаю, он здесь более уместен)
- superposeur
Бо́льшая часть ценности доказательства заключается в разработке математических определений и промежуточных теорем, необходимых для его получения, в стиле Гротендика. Эта способность, похоже, всё ещё недоступна ИИ (по крайней мере, я не слышал о каких-либо принципиально новых и полезных определениях, таких как «схема» или «модулярная форма», появившихся в последнем потоке доказательств, созданных ИИ). НО, интересно, мог бы ИИ развить этот навык с помощью процесса эффективного рефакторинга большого доказательства в Lean на части, а затем интерпретации этих частей обратно в новые, понятные человеку определения с запоминающимися названиями?
- mcapodici
Вот это времена настали.
https://github.com/anthropics/fermats-last-theorem/blob/main...
- chvid
Я думаю, что интересная задача, возможно, даже более интересная, — это найти самое короткое / самое сжатое / самое лёгкое для понимания (формально проверяемое) доказательство.
- rawling
Обсуждение на главной странице: https://news.ycombinator.com/item?id=49568506