Томас Хейлс о Lean: автоформализация стала практикой, а ошибки в ядре нашёл ИИ

Томас Хейлс в гостевом посте разбирает два вопроса: насколько практичной стала автоформализация (перевод математических доказательств искусственным интеллектом в формальный код) и насколько надёжна система Lean, в которой этот код чаще всего пишут. Формальное доказательство, объясняет он, проверено на уровне оснований математики и правил логики; из-за числа шагов такую проверку делает компьютер. Среди математиков, по словам Хейлса, Lean, самая популярная из систем доказательств, поэтому пост посвящён ей.

Lean разработал и представил Лео де Мура в 2013 году, когда работал в Microsoft; он убедил компанию сделать код открытым. Первым пользователем, по книге Кевина Хартнетта «The Proof in the Code», был Джереми Авигад. В 2017 году его аспирант Марио Карнейро вместе с Йоханнесом Хёльцлем выделил из основной библиотеки Lean отдельную математическую библиотеку mathlib. Сегодня в ней почти 300 000 теорем, более 100 000 определений, 2,5 млн строк кода и более 700 участников.

Раньше доказательства с бумаги переписывали в формальный вид вручную: формальное доказательство гипотезы Кеплера (об упаковке шаров в трёхмерном пространстве) заняло около 20 человеко-лет и состоит примерно из 500 000 строк. Хейлс заявляет, что в 2026 году автоформализация стала практической реальностью, и приводит вехи. Сентябрь 2025: Math Inc. получила «квази-автоформализацию» теоремы о распределении простых чисел, людям приходилось подсказывать ИИ, когда он застревал. Январь 2026: препринт J. Urban «130k lines of formal topology in two weeks» об автоформализации крупных частей учебника топологии Мункреса. Март 2026: Math Inc. автоформализовала упаковку шаров в 24 измерениях; проект дал около 500 тыс. строк, после сокращения кода, около 200 тыс. Май 2026: группа в Meta/Facebook Research в проекте ATLAS автоформализовала значительную часть 26 учебников по математике. Особо Хейлс отмечает автоформализацию Великой теоремы Ферма, о которой Anthropic объявила 4 сентября: 13 млн строк на Lean за 11 дней. Анонс OpenAI от 8 сентября о возникновении сингулярности в уравнениях Навье, Стокса при наличии внешней силы сопровождался автоформализацией этой теоремы в Lean. В тот же день, 8 сентября 2026 года, Джаред Лихтман объявил о запуске MAP (Mathematics Autoformalization Project), цель которого, перевести «всю известную математику в формальный код».

О надёжности. Ядро Lean, несколько тысяч строк на C++: тщательно спроектированное, но крайне сложное. Библиотека mathlib проходит проверку ядром, и если в её 2,5 млн строк затесалось безусловно ложное доказательство, виновато ядро или среда выполнения, не отвергшие его. Хейлс настаивает: доказательствам в Lean не следует верить, пока их не проверило ядро, а после этого нужен ещё и человеческий аудит соответствия формулировки, доказана ли именно та теорема, что мы имеем в виду и правильно ли определены понятия. Эта задача, по его словам, как правило, несоизмеримо проще проверки самого доказательства. Для Навье, Стокса человек должен сверить формулировку в Lean с формулировкой Феффермана для задачи тысячелетия и проверить определения вещественных чисел, частных производных и меры; в этом помогает инструмент comparator, который заодно ищет посторонние аксиомы.

Наконец, «Summer of Soundness Bugs». Ошибка корректности (soundness bug), дефект ядра, позволяющий доказать ложное утверждение, а значит, любое. По Хейлсу, для системы доказательств это самая катастрофическая ошибка. Он сам нашёл такую в HOL Light в 2003 году: ядро той системы, всего несколько сотен строк. В Lean 4 до выпуска в сентябре 2023 года нашли и исправили две такие ошибки, в мае 2025 года сообщили ещё об одной (переполнение). Летом 2026 года, в июле и августе, обнаружили несколько новых; одна из них позволяла незаконно опровергнуть гипотезу Коллатца, а Хейлс узнал о ней, когда она выдала короткое незаконное доказательство гипотезы Кеплера в Lean. Все ошибки быстро исправлены, mathlib перепроверена исправленным ядром, анализ дан в разборе де Мура. Хейлс считает находки хорошим знаком: их выявил передовой ИИ в руках исследователей безопасности, заинтересованных в надёжных ядрах, а не взломщики. Ошибку с гипотезой Коллатца нашёл Рамана Кумар, соавтор работы о верифицированной реализации ML CakeML; несколько ошибок нашёл Дэн Селсам. Доступный текст поста обрывается на этом месте.

Ключевые факты

• Хейлс считает, что в 2026 году автоформализация стала практической реальностью: Anthropic объявила об автоформализации Великой теоремы Ферма (13 млн строк на Lean за 11 дней), а анонс OpenAI по уравнениям Навье, Стокса сопровождался формализацией в Lean.
• Для сравнения: формальное доказательство гипотезы Кеплера, написанное людьми, заняло около 20 человеко-лет и примерно 500 000 строк; автоформализация упаковки шаров в 24 измерениях дала около 500 тыс. строк, сокращённых позднее до около 200 тыс.
• Правило Хейлса: доказательствам в Lean не следует верить, пока их не проверило ядро, и принимать их не следует до человеческого аудита соответствия формулировки; этот аудит, по его словам, как правило, несоизмеримо проще проверки доказательства.
• Летом 2026 года в Lean нашли несколько ошибок корректности (в июле и августе), одна из них давала незаконное опровержение гипотезы Коллатца; все исправлены, mathlib (почти 300 000 теорем, 2,5 млн строк) перепроверена исправленным ядром.
• Ошибки выявил передовой ИИ в руках исследователей безопасности, а не взломщиков, и Хейлс называет это положительным развитием событий.

Почему это важно

Стоимость формализации резко меняется: то, на что у людей уходили десятки человеко-лет (гипотеза Кеплера, около 20), ИИ теперь делает за дни, 13 млн строк на Lean за 11 дней в случае Великой теоремы Ферма. Но чем больше кода пишет ИИ, тем меньше шансов, что кто-то прочтёт его глазами, и вся надёжность ложится на небольшое ядро проверки. Пост Хейлса объясняет, на что именно опирается доверие к таким доказательствам и где у него слабые места, и это разговор не только о Lean, но и о том, как принимать результаты, созданные ИИ.

Кому это важно

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

Как это применить

Практическая рекомендация автора двухступенчатая. Первое: не считать доказательство в Lean достоверным, пока оно не прошло проверку ядром. Второе: до принятия результата провести человеческий аудит соответствия формулировки, проверить, что доказанная теорема в Lean совпадает с задуманной и что базовые понятия (вещественные числа, частные производные, мера) определены корректно. В этом помогает инструмент comparator, он же проверяет, не добавлены ли посторонние аксиомы.

Можно ли доверять

Это авторское эссе одного специалиста, а не новое исследование с измерениями. Хейлс, давний практик формализации: он участвовал в семинаре по Lean в 2015 году и сам нашёл ошибку в HOL Light в 2003 году. Оценки вроде «автоформализация стала практической реальностью», его суждение; факты о проектах и датах он приводит с названиями компаний и авторов. Редакторская пометка с подписью «T.» сообщает, что пост был написан в другом формате и конвертирован с помощью ИИ. Текст, с которого сделан этот пересказ, обрывается на полуслове в разделе о летних ошибках, поэтому выводы и заключительная часть поста здесь не отражены.

Риски и подводные камни

Главный риск, ошибка корректности в ядре: она позволяет доказать ложное утверждение, а значит любое. Ядро Lean, несколько тысяч строк на C++ (у ядра HOL Light, по словам автора, всего несколько сотен строк), и Хейлс называет его тщательно спроектированным, но крайне сложным. Второй риск, разрыв между доказанным и задуманным: формально верное доказательство может относиться не к той теореме, поэтому нужен аудит формулировки. Отдельно: в доступной части текста не сказано, что формализации Великой теоремы Ферма от Anthropic и Навье, Стокса от OpenAI уже прошли такой человеческий аудит.

«Доказательствам в Lean не следует верить, пока они не проверены ядром.»

— Томас Хейлс, гостевой пост

Компания Meta Platforms признана экстремистской организацией, её деятельность на территории РФ запрещена.