Терренс Тао написал для математиков о надёжности Lean и роли ИИ

9 октября 2026 года Терренс Тао выложил в блоге пост «What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI». Адресат понятен по названию: профессиональные математики, которые присматриваются к формальной верификации и к ИИ-системам, пишущим доказательства. На Hacker News запись набрала 53 очка и 7 комментариев. В нашу ленту пришла только ссылка, без текста, поэтому аргументы автора мы не пересказываем. Ниже разобран контекст, в котором такой пост появляется и почему он важен.

Почему вопрос о надёжности стал практическим

Lean начинался как проект Леонардо де Моуры в Microsoft Research в 2013 году. Сегодня это рабочий инструмент для больших коллективных работ. Сам Тао в конце 2023 года участвовал в формализации гипотезы PFR, и она заняла около трёх недель. В 2024 году он координировал Equational Theories Project: нужно было определить 22 028 942 импликации между 4694 тождествами на магмах. Без автоматики и формальной проверки такой объём не осилили бы ни люди, ни рецензенты.

Параллельно в Lean начали работать языковые модели. В июле 2024 года AlphaProof от Google DeepMind решила четыре из шести задач IMO и набрала 28 баллов из 42. Доказательства она выдавала на Lean. С тех пор вопрос «можно ли верить тому, что вышло из такой цепочки» относится уже не к философии математики, а к повседневной работе.

Где проходит граница доверия

У Lean есть небольшое ядро, которое проверяет каждый терм доказательства. Тактики, автоматизация и сгенерированный моделью код стоят снаружи ядра. Если они ошибутся, ядро просто отвергнет результат. Это и делает связку с ИИ привлекательной: галлюцинация в доказательстве ловится механически.

Остаются места, где доверие нужно оценивать отдельно:

• Формулировка теоремы. Ядро подтверждает, что доказано написанное утверждение. Совпадает ли оно с задуманным, решает человек.
• Определения. Неточное определение в библиотеке или в файле делает доказанную теорему бессодержательной.
• Аксиомы. Lean опирается на `propext`, `Classical.choice` и `Quot.sound`. Команда `#print axioms` показывает, какие использованы.
• `sorry`. Это заглушка вместо доказательства. Файл с ней компилируется, но теорема не доказана.
• `native_decide`. Тактика добавляет в базу доверия компилятор, и в списке аксиом появляется `Lean.ofReduceBool`.
• Реализация ядра. Существуют независимые проверяющие программы, например lean4checker и сторонние перепроверки, снижающие риск ошибки в самом ядре.

Что меняет ИИ

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

Из этого следует практический вывод: аудит смещается с шагов доказательства на условия задачи. Для математиков это скорее смена навыка, чем потеря контроля.

Как с этим работать

Если вы собираетесь использовать Lean или ИИ-ассистента в исследовательской работе, полезно придерживаться короткого порядка действий:

• Формулировки теорем пишите или перечитывайте сами, даже если доказательство сгенерировано моделью.
• Перед публикацией запускайте `#print axioms` и ищите `sorry`.
• Проверяйте, что используемые определения из Mathlib соответствуют вашему пониманию. Для нестандартных случаев пишите контрпримеры и проверочные леммы.
• Для критичных результатов прогоняйте файл через независимый проверяющий инструмент.
• Читайте оригинальный пост Тао. Здесь мы дали контекст, а его аргументы и рекомендации лучше брать из первоисточника.