Терри Тао: математикам стоит знать о ненадёжности Lean
What mathematicians should know about the Lean Theorem Prover: reliability & AI
Томас Хейлз разбирает, почему Lean стал главным инструментом формальной математики, но требует осторожности. Autoformalization уже реален: Fermat's Last Theorem сгенерировали 13 млн строк Lean за 11 дней, а Navier-Stokes — с принуждением. Однако «лето багов корректности» 2026 года показало: ядро Lean может пропустить ложное доказательство. Хейлз призывает к человеческому аудиту утверждений и проверке ядра.
Летние баги были обнаружены передовыми ИИ-моделями в руках исследователей безопасности, заинтересованных в надёжных ядрах, а не чёрными хакерами.
- chr15m
Увидим ли мы когда-нибудь снова баг в ядре Lean, связанный с надёжностью?
Для разработчика ПО этот вопрос кажется безумным. В прошлом были баги, конечно, будут и ещё.
Когда мы увидим эти баги, что они будут значить для доказательств на Lean, сгенерированных ИИ? Можем ли мы им доверять?
Всё это сводится к доверию.
Мы можем в высокой степени доверять человеческим проверкам благодаря сообществу, репутации и человеческому proof-of-work. Люди иногда лгут о математических результатах, но это редкость именно из-за этого. Они совершают ошибки, и эти ошибки обнаруживаются сообществами, которые сами по большей части заслуживают доверия по той же причине.
LLM не заботятся о репутации. Они галлюцинируют и фабрикуют часто. В обвязках они буквально пытаются жульничать и обходить правила, что катастрофично для знаний, закодированных в правилах. Поэтому нам приходится полагаться на проверяльщики доказательств.
Проблема в том, насколько можно доверять проверяльщикам доказательств? Есть ли в них баги? И свободна ли сама лежащая в основе теория от парадоксов, неразрешимых утверждений и математических «багов», которые можно эксплуатировать? Представьте математика-человека, одержимого идеей обмануть других математиков — стали бы мы доверять его прорывам, даже при наличии верификатора?
Из-за этих свойств последней линией обороны должны быть люди, укоренённые в сообществе и системе человеческого доверия, основанной на proof-of-work. На данный момент люди слишком сильно доверяют инструментам.
Предсказание: баги будут найдены людьми с помощью ИИ-инструментов, что поставит под сомнение доказательство гипотезы Навье — Стокса.
- rramadass
В статье уже упоминается работа Sets in Types, Types in Sets Бенджамина Вернера, которая устанавливает соответствие между теориями множеств и типов.
Ещё одна связанная и более доступная статья об эволюции теории типов и её связи с теориями множеств и категорий — Types, Sets and Categories Джона Белла.
Наконец, см. также Typed Lambda Calculus / Calculus of Constructions Хельмута Брандла — превосходный обзор CoC/CIC объёмом с книгу, но при этом сжатый.
По моему мнению, всё вышеперечисленное обязательно к прочтению для понимания систем доказательства теорем и ассистентов доказательств. В частности, работа Брандла — маст-рид.
- JonChesterfield
> Автоформализация стала практической реальностью в 2026 году
Хм, _может быть_. Последнюю неделю я переводил статьи в Lean, и соответствие между формализованным результатом и статьями крайне плохое. Цикл, похоже, такой: «попробуем взяться за статью, она сложновата, докажем что-нибудь другое, объявим об успехе». Это всё ещё быстрее, чем делать всё вручную, но статья на входе -> Lean на выходе никоим образом не гарантирует соответствия между ними.