Основная идея Lean, который доминирует для проверки современных математических гипотез, состоит в том, что логику дедукции можно записать в виде специального языка программирования. Простая математическая теорема на Lean будет выглядеть примерно так:
theorem add_zero (n : Nat) : n + 0 = n := by
induction n with
| zero => rfl
| succ n ih => simp [Nat.add_succ, ih]
Потом ядро Lean просто двигается по цепочкам дедуктивных выводов и проверяет, что по типам результатов есть совпадения, т.е. шаги реально логически доказаны. Это и есть та самая «логика первого порядка», о которой говорит Цимерман.
Проблема для людей в том, что ИИ для доказательства части новых математических гипотез использует тысячи или сотни тысяч таких логических операций. Они проходят автоматическую проверку Lean на корректность выводов, но разум кожаных математиков просто не может осознать такой масштаб логических цепочек дедукции. Получается примерно как с нейросетью: вроде понятно, как работают отдельные нейроны, но это никак не даёт понимания, как нейросеть работает в целом.
Почему ИИ так стали мощны в самой сложной логике вообще известной людям — математической? Дело как раз в этом Lean. На обучении модели сразу генерируют цепочки дедукции в Lean, а Lean сообщает обратно модели просто идеальный reward signal о том, верно или нет рассуждение в целом, а также диагностику логических ошибок.
Очень интересным тут стал новый тренд в ИТ-разработке в духе: «а нельзя ли также описать, как у математиков, через Lean спецификации на код и получить 100% точное математическое доказательство, что код соответствует спецификации?»
Можно, и даже делается. Пока Lean-проверки кода программ сосредоточены больше в части разработчиков криптографических систем. Там уже становится де-факто стандартом необходимость Lean-доказательства, что криптографический алгоритм устойчив к взлому.
Последняя масштабная работа:
«A benchmark for vericoding: formally verified program synthesis (POPL 2026)» анализирует 12 504 формальные спецификации, из которых 7 141 — на Lean. В отличие от обычного «vibe coding» (генерация кода из естественного языка), здесь ИИ должен сгенерировать машинно-проверяемое доказательство того, что код соответствует спецификации.
Результаты оказались отрезвляющими: успешность LLM в Lean составила всего 27%, тогда как в Verus/Rust — 44%, а в Dafny — 82%. Это наглядно показывает, что явное построение доказательств в Lean — существенно более сложная задача для современных моделей, но с другой стороны надёжность Lean-проверок несоразмерно выше других методов.
📌 За этой областью исследований нужно минимум наблюдать, т.к. из неё могут прийти строгие форматы оформления спецификаций на код для ИИ, которые могут проходить Lean-проверки. После чего тестировщики могут идти работать в Макдональдс, т.к. тестирование для таких алгоритмов уже не предполагается. Математически доказана их безошибочность по такой же строгости, как доказана математическая теорема.
https://arxiv.org/abs/2509.22908