Claude за 11 дней доказал великую теорему Ферма — впервые в полностью проверяемом компьютером виде

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

^ этот раздел, по моему мнению, должен был быть в первых нескольких абзацах. Объяснение того, почему это важно, не должно быть так далеко.

"Доказательство — это не современное доказательство, которое я сам формализую, следуя идеям Кхаре, Тейлора и др., а изложение Дармона–Даймонда–Тейлора 1995 года аргумента Уайлса–Тейлора–Уайлса через теорему Ленглендса–Таннелла и теорему Рибета о понижении уровня. Репозиторий Anthropic развивает теорию Фонтейна (для изучения плоских деформаций представлений Галуа) и развивает достаточно работ Мазура об идеале Эйзенштейна, чтобы заключить, что никакая кривая Фрея не может иметь точку порядка p>=17. Это означает, что их доказательство FLT работает только для p>=17, однако FLT уже была формализована для нечетных регулярных простых чисел Бестом–Биркбеком–Браской–Родригесом, а наименьшее иррегулярное простое число — 37, так что все в порядке."

Мой вопрос любому математику, читающему это: имеет ли вышесказанное хоть какой-то смысл?

Я спрашиваю потому, что могу читать большинство технических материалов, связанных с компьютерной инженерией, программированием, спецификациями оборудования и т.д. Даже если я не полностью понимаю все детали, я могу довольно хорошо следить за ними. Поэтому мне интересно, могут ли профессиональные математики взглянуть на вышесказанное и все же понять его, как опытные инженеры-программисты понимают компьютерные вещи.

> Попутно было написано 13 миллионов строк на Lean и доказано 29 500 промежуточных теорем.

Довольно безумно. Полагаю, это еще раз подтверждает идею, что все, что можно показать как правильное, может быть сделано моделью.

> команда агентов завершила доказательство чуть менее чем за две недели, потребив около шести миллиардов выходных токенов от универсальной внутренней исследовательской модели, примерно сопоставимой с Claude Fable 5.1.

При цене $50 за миллион выходных токенов это обошлось бы примерно в $300 тысяч (плюс немного за входные/префиксные токены) по тарифам API.

Кстати, я настоятельно рекомендую эту книгу Саймона Сингха.

https://en.wikipedia.org/wiki/Fermat's_Last_Theorem_(book)

13 миллионов строк кода — вы уверены, что он не использовал какие-либо скрытые проблемы в системе доказательств Lean?

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

Я с оптимизмом ожидаю, что стану свидетелем появления глобальной "панацеи" при своей жизни благодаря усилиям ИИ. Экономически эффективная крупномасштабная генная инженерия, лекарство от каждой болезни, возможно, даже лекарство от старения.

Будущее одновременно прекрасно и ужасно.

С учетом того, насколько способной и дешевой становится автоматическая проверка доказательств, мне интересно, сколько доказательств, которые почти все математическое сообщество считает истинными, будут признаны ложными. И не из-за какой-то незначительной легко исправимой ошибки, а из-за фундаментального изъяна в рассуждениях.

Ладно, давайте запустим стаю бешеных агентов на P = NP? дальше!