Lean

Lean
Тип	Интерактивная система доказательства теорем, функциональный язык программирования
Автор	Леонардо де Моура
Разработчики	Lean Focused Research Organization, сообщество Lean
Написана на	Lean (преимущественно, начиная с Lean 4)
Операционные системы	Linux, macOS, Windows
Языки интерфейса	английский
Дата выпуска	16 июня 2014
Аппаратные платформы	x86-64 и AArch64
Последняя версия	4.35.0 (12 октября 2026)
Репозиторий	github.com/leanprover/le…
Читаемые форматы файлов: Lean 3 file format и Lean 4 file format
Создаваемые форматы файлов: Lean 3 file format и Lean 4 file format
Лицензия	Apache License 2.0
Сайт	lean-lang.org

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

Разработка Lean началась в 2013 году под руководством Леонардо де Моуры в Microsoft Research. Первая официальная версия опубликована в 2014 году, Lean 3 — в 2017-м, а Lean 4.0 — в 2023-м. В четвёртой версии система в значительной степени реализована на самом языке Lean и используется не только для доказательств, но и для написания исполняемых программ и расширений среды разработки.

Существенную роль в использовании Lean математиками играет развиваемая сообществом библиотека Mathlib, содержащая формальные определения, теоремы и средства автоматизации. Lean применяют также для формальной верификации программ и в исследованиях автоматического доказательства теорем. Возможности системы используются в математическом образовании. В 2025 году проект получил премию ACM SIGPLAN Programming Languages Software Award.

История

Первые версии

Леонардо де Моура начал разрабатывать Lean в Microsoft Research в 2013 году. Замысел состоял в том, чтобы соединить надёжность проверки доказательств небольшим логическим ядром с удобством автоматических процедур вывода и масштабируемостью, необходимой для больших математических и программных проектов. Версия Lean 0.1 официально вышла 16 июня 2014 года; устройство системы было изложено разработчиками в публикации 2015 года The Lean Theorem Prover (System Description).

Ранние версии использовали библиотеку на C++, а способы взаимодействия с системой постепенно менялись: от программного интерфейса и тактик на Lua к собственному языку команд и тактик. Lean 3.0 вышел 20 января 2017 года. В нём расширения системы — в частности, новые тактики и обозначения — можно было писать непосредственно на Lean. В этот же период вокруг системы сложилось сообщество математиков, приступившее к созданию библиотеки Mathlib.

Lean 4

Разработка Lean 4 началась в 2018 году. Проект был переосмыслен как сочетание системы доказательств и полноценного функционального языка программирования; значительную часть прежней реализации на C++ заменили кодом на Lean. Такой подход позволяет использовать общие механизмы языка для построения программ, тактик и новых синтаксических конструкций. Разработчики описали эту архитектуру в статье 2021 года; тогда же стали доступны ранние версии Lean 4.

Официальная версия Lean 4.0 вышла 8 сентября 2023 года. В 2023 году на Lean 4 была перенесена и библиотека Mathlib. В июле того же года создана некоммерческая организация Lean Focused Research Organization (Lean FRO), занимающаяся развитием программной системы, её производительности, средств автоматизации и доступности для пользователей.

Логические основы и проверка доказательств

Теория типов

Логическая основа Lean — разновидность исчисления конструкций с индуктивными типами и зависимыми типами. В такой системе тип выражения может зависеть от значения другого выражения: например, тип вектора может включать его длину. Это позволяет описывать в одной формальной системе как вычислительные объекты, так и утверждения об этих объектах.

Lean использует принцип «высказывания как типы» — форму соответствия Карри — Ховарда. Логическое высказывание рассматривается как тип, а его доказательство — как терм этого типа. Например, доказательство импликации P → Q может быть представлено функцией, которая преобразует доказательство P в доказательство Q. Система проверяет соответствие типа построенного терма типу заявленного утверждения.

Предложения в Lean принадлежат особому сорту Prop; для типов данных служат иерархии Type. Индуктивные определения задают объекты через допустимые конструкторы, например натуральные числа — через нуль и операцию последовательного перехода к следующему числу. С ними связаны рекурсивные функции и доказательства по индукции. При формализации классической математики можно использовать аксиомы классической логики; проверка остаётся относительной к принятому набору аксиом.

Логическое ядро и тактики

Исходный текст на Lean сначала разбирается как синтаксическая конструкция. Затем элаборатор (англ. elaborator) преобразует удобную пользователю запись с неявными аргументами, обозначениями и сокращениями во внутреннее представление на языке теории типов. Проверку полученного доказательного терма выполняет логическое ядро (англ. kernel). Разделение сложных средств ввода и автоматизации и сравнительно небольшого проверяющего ядра является одним из основных принципов архитектуры Lean.

Тактика (англ. tactic) — команда, применяемая при построении доказательства. Тактики позволяют последовательно преобразовывать текущую цель: вводить предположения, разбирать случаи, применять ранее доказанные утверждения, переписывать выражения по равенствам или вызывать автоматические процедуры. Их результат, как и доказательство, непосредственно записанное в виде терма, проходит проверку ядром. Поэтому ошибки в обычной реализации тактики, как правило, приводят к невозможности построить принимаемое доказательство, а не к изменению логических правил.

Такой подход отличает интерактивное доказательство от полностью автоматического поиска: пользователь может задавать стратегию и промежуточные шаги, а повторяющиеся операции поручать системе. В результате одни доказательства имеют форму коротких выражений, другие — последовательностей тактик или комбинаций обоих способов.

Что гарантирует проверка

Принятие доказательства ядром означает, что построенный формальный терм имеет требуемый тип в окружении принятых определений, теорем и аксиом. Такая проверка не удостоверяет сама по себе ни соответствия формулировки на Lean исходному неформальному математическому утверждению, ни обоснованности всех использованных аксиом. При неточном определении или неверном переводе теоремы система может принять доказательство утверждения, отличного от того, которое намеревался доказать математик.

Достоверность формальной проверки также зависит от используемых аксиом и доверия к средствам проверки. Команда #print axioms позволяет выяснить, на каких аксиомах основана конкретная теорема; среди возможных зависимостей встречаются недоказанные допущения и служебная аксиома sorryAx, связанная с оставленными без доказательства местами. Для ответственных проектов предусмотрены дополнительные способы перепроверки результатов, в том числе независимыми реализациями ядра. Документация Lean особо различает обычную ошибку в доказательстве и намеренно вводящий в заблуждение код.

Lean 4 как язык программирования

Lean 4 — статически типизированный функциональный язык, предназначенный не только для построения доказательств, но и для разработки исполняемых программ. Он поддерживает пользовательские типы данных, сопоставление с образцом, рекурсию, функции высшего порядка, обобщённые определения и классы типов. В языке есть средства для программ с вводом-выводом, обработки изменяемого состояния и эффективного выполнения вычислений.

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

Lean допускает использование математических символов Юникода непосредственно в программе, в том числе знаков ∀, ∃, →, ∧ и ℕ. В поддерживаемых редакторах предусмотрены способы ввода таких символов через текстовые последовательности, близкие к командам LaTeX.

Библиотеки и средства разработки

Mathlib

Mathlib (также mathlib) — открытая библиотека формализованной математики для Lean, создаваемая и сопровождаемая сообществом отдельно от основной программной системы. Её развитие началось в 2017 году. В отличие от набора несвязанных примеров доказательств, Mathlib организована как общая база определений, теорем, иерархий математических структур и средств автоматизации. Она используется как основа для последующих формализаций в алгебре, анализе, геометрии и других областях.

Авторы коллективной статьи The Lean Mathematical Library (2020) особо выделяли ориентацию библиотеки на классическую математику, использование зависимых типов, переиспользуемые иерархии математических структур, сочетание локальной и более масштабной автоматизации и распределённую организацию работы. Библиотека развивается с участием многих математиков и программистов, поэтому её состав и объём постоянно меняются. Цифры, относящиеся к прежним версиям Mathlib, не характеризуют автоматически её последующие редакции.

Переход Mathlib на Lean 4 в 2023 году был самостоятельной задачей сообщества. Наличие библиотеки делает возможным построение новых доказательств с опорой на ранее проверенные результаты, но Mathlib не тождественна ни логическому ядру, ни языку Lean и не охватывает автоматически всю опубликованную математику.

Инструменты

Для работы с Lean 4 используется, в частности, Visual Studio Code с расширением Lean 4, предоставляющим подсветку синтаксиса, сведения о текущих целях доказательства, сообщения об ошибках и другие функции интерактивного редактирования. Взаимодействие с редактором позволяет наблюдать изменения целей по мере построения доказательства.

В состав инструментальной экосистемы входят Lake — средство сборки проектов, управления пакетами и зависимостями — и Elan, предназначенный для установки и выбора версий Lean. Они обслуживают проекты с исходными файлами на Lean, но не являются заменой математической библиотеки Mathlib или логического ядра.

Применение

Формализация математики

Lean используют для формальной записи и проверки результатов как учебной, так и современной исследовательской математики. Формализация требует явно задать математические объекты, формулировки утверждений и шаги вывода, которые в обычном изложении могут оставаться неявными. Mathlib обеспечивает многие необходимые определения и ранее проверенные результаты; для специальных задач исследователи создают дополнительные библиотеки и формальные разработки.

Один из известных примеров — Liquid Tensor Experiment, связанный с теоремой из теории конденсированной математики, развиваемой Петером Шольце совместно с Дастином Клаузеном. Формализация центральной теоремы о так называемых жидких векторных пространствах была проведена командой под руководством Йохана Коммелина с математической поддержкой Шольце. О важном промежуточном результате сообщалось в 2021 году, а завершение проекта объявлено 14 июля 2022 года. В работе участвовал, в частности, Кевин Базард. Проект использовал Lean и Mathlib, но не был частью образовательного проекта Xena.

Другой пример — проект формализации доказательства полиномиальной гипотезы Фреймана — Ружи в варианте для векторных пространств над полем из двух элементов; работа проводилась при участии Теренса Тао и сообщества Lean. Для неё потребовалась, в частности, формализация неравенств для энтропии Шеннона. Проект выполнялся на Lean 4; его материалы опубликованы вместе с формальными исходными текстами.

К смежным инициативам относится Formal Abstracts, инициированный в 2017 году математиком Томасом Хейлзом. Замысел проекта состоял в формальной записи основных определений и формулировок результатов научных публикаций без обязательной формализации их доказательств. В опубликованном описании Lean указан как формальная основа, а сама инициатива охарактеризована как проектируемый сервис с экспериментальными разработками.

Проверка программ и автоматизированное рассуждение

Зависимые типы и возможность строить формальные доказательства позволяют использовать Lean для проверки свойств программ и алгоритмов. При такой работе спецификация ожидаемого поведения выражается формальным утверждением, а проверка устанавливает соответствие построенного доказательства этой спецификации. В обосновании премии ACM SIGPLAN 2025 года среди промышленных применений Lean названы верификация языка управления доступом Cedar, проверка генератора выборок SampCert, предназначенного для задач дифференциальной приватности, а также проекты проверки блокчейн-систем.

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

Образование и проект Xena

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

В 2017 году Кевин Базард организовал в Имперском колледже Лондона проект Xena (Xena Project), первоначально ориентированный на вовлечение математиков, прежде всего студентов, в использование систем проверки доказательств. Участники предлагали рассматривать задания университетских курсов как задачи, решаемые в Lean; для этого использовались, среди прочего, игровые учебные материалы Natural Number Game. Позднее Базард писал, что его собственные интересы сместились к формализации более сложных математических результатов.

Примеры кода

Ниже приведены краткие примеры синтаксиса Lean 4. Для определения собственных натуральных чисел можно задать индуктивный тип с двумя конструкторами: нулём и последовательным переходом к следующему числу. Стандартный тип Nat уже имеется в библиотеке Lean, поэтому здесь используется новое имя UnaryNat.

inductive UnaryNat where
  | zero : UnaryNat
  | succ : UnaryNat → UnaryNat

В качестве обычной функции на встроенном типе натуральных чисел можно определить удвоение числа. Команда #eval вычисляет значение выражения.

def twice (n : Nat) : Nat := n + n

#eval twice 7

Следующий пример задаёт и доказывает утверждение о перестановке членов конъюнкции. После by следуют тактики: intro вводит гипотезу, а exact предъявляет доказательство требуемой цели. Обозначение ⟨h.2, h.1⟩ строит доказательство конъюнкции в обратном порядке из двух частей исходной гипотезы.

theorem and_swap (p q : Prop) : p ∧ q → q ∧ p := by
  intro h
  exact ⟨h.2, h.1⟩

Тот же результат можно записать без явного перечисления тактик, непосредственно построив доказательный терм:

theorem and_swap_term (p q : Prop) : p ∧ q → q ∧ p :=
  fun h => ⟨h.2, h.1⟩

Оба способа выражают одно логическое содержание; различается форма записи доказательства. Эти примеры иллюстрируют базовые возможности языка, а не приёмы проверки крупных математических работ.

Значение и ограничения

Развитие Lean стало одним из заметных направлений компьютерной формализации математики. При присуждении премии ACM SIGPLAN Programming Languages Software Award в 2025 году были отмечены сочетание теоретических и инженерных решений системы, применение в математических исследованиях и проверке программ, а также возникновение вокруг Mathlib активного сообщества.

Одновременно формализация остаётся трудоёмкой деятельностью: для проверки сложного результата обычно недостаточно переписать опубликованный текст в другой нотации; требуется формально определить используемые понятия, установить множество вспомогательных утверждений и устранить шаги, которые обычное математическое изложение оставляет читателю. Не все математики считают желательным превращение полной формализации в универсальную норму публикации: в обсуждениях отмечаются различия между проверкой логической корректности, объяснением математической идеи и поиском новых результатов.

Таким образом, машинная проверка в Lean даёт сильную гарантию для определённым образом записанного формального вывода при заданных допущениях, но не отменяет необходимость проверять смысл формализации, происхождение аксиом и адекватность самих определений. Возможности автоматизации и объём доступных библиотек также зависят от области математики и текущего состояния экосистемы Lean.

См. также

• Инструмент интерактивного доказательства теорем
• Формальная верификация
• Зависимый тип
• Соответствие Карри — Ховарда
• Coq
• Isabelle
• Agda

Литература

• L. de Moura; S. Kong; J. Avigad; F. van Doorn; J. von Raumer. The Lean Theorem Prover (System Description) (англ.) // Automated Deduction — CADE-25. — Springer, 2015. — Vol. 9195. — P. 378–388. — doi:10.1007/978-3-319-21401-6_26.
• L. de Moura; S. Ullrich. The Lean 4 Theorem Prover and Programming Language (англ.) // Automated Deduction — CADE-28. — Springer, 2021. — Vol. 12699. — P. 625–635. — doi:10.1007/978-3-030-79876-5_37.
• The mathlib Community. The Lean Mathematical Library (англ.) // Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020). — ACM, 2020. — P. 367–381. — doi:10.1145/3372885.3373824.
• P. Iannone; G. Marasingha; A. Thoma. Teaching Mathematics with Lean: Interactive Theorem Provers in the Classroom (англ.) // Notices of the American Mathematical Society. — 2025. — Vol. 72, no. 7. — P. 740–747. — doi:10.1090/noti3184.
• L. Sloman. In Math, Rigor Is Vital. But Are Digitized Proofs Taking It Too Far? (англ.) // Quanta Magazine. — 2026. — 25 March.

Ссылки

• Lean (англ.). Lean Lang.
• The Lean Language Reference (англ.). Lean Lang.
• Theorem Proving in Lean 4 (англ.). Lean Lang.
• Christiansen, David Thrane. Functional Programming in Lean (англ.). Lean Lang.
• Lean community / Mathlib (англ.). Lean community.
• The Xena Project (англ.). Imperial College London.