Lean 4

Lean 4 — proof assistant, разработанный Leonardo de Moura (Microsoft Research, затем Lean FRO). Четвёртая версия, переписанная с нуля в 2021 году. Компилируется в C, self-hosting (компилятор Lean написан на Lean).

Теоретическая основа — Calculus of Inductive Constructions (CIC): зависимые типы, индуктивные типы, иерархия универсумов ($\text{Prop} : \text{Type}_0 : \text{Type}_1 : \ldots$).

Lean реализует соответствие Карри — Ховарда:

Пример: утверждение $A \land B \Rightarrow B \land A$ — это тип функции $A \times B \to B \times A$. Доказательство — терм $\lambda \langle a, b \rangle \mapsto \langle b, a \rangle$. Верификатор проверяет, что этот терм имеет заявленный тип.

Ядро верификатора

Ядро Lean (kernel) — ~5 000 строк C++. Выполняет три операции:

1. Type checking. Для данного терма $e$ и типа $T$ — проверить, что $\vdash e : T$.
2. Definitional equality. Для типов $T_1, T_2$ — проверить, что $T_1 \equiv T_2$ (равенство по определению через $\beta$-, $\delta$-, $\iota$-редукцию).
3. Reduction. Вычисление нормальных форм ($\beta$-редукция: $(\lambda x.\, b)\, a \to b[x := a]$, $\delta$-редукция: подстановка определений, $\iota$-редукция: вычисление match-выражений).

Принцип де Брёйна: тактики, автоматизация (simp, omega, ring, aesop) и все надстройки генерируют proof terms. Но каждый proof term обязательно проходит через ядро. Ошибка в тактике не приводит к некорректному доказательству — ядро отвергнет невалидный терм.

Soundness

Для CIC доказаны:

1. Strong normalization. Каждое вычисление в системе типов завершается. Проверка типов всегда даёт ответ.
2. Consistency. Невозможно построить терм типа $\bot$ (False). Утверждение $\bot$ ненаселено — нельзя «доказать» ложь.
3. Decidability of type checking. Проверка $\vdash e : T$ — разрешимая процедура. Результат детерминирован.

Lean 4 использует три аксиомы, не доказуемые в чистом CIC:

1. $\text{propext}$: $(P \leftrightarrow Q) \to P = Q$ (extensionality высказываний)
2. $\text{Quot.sound}$: корректность фактор-типов
3. $\text{Classical.choice}$: аксиома выбора + закон исключённого третьего

Непротиворечивость этих аксиом доказана через модели в ZFC.

Как работает MathProver

Агент генерирует proof term, ядро Lean проверяет его тип. Если тип не совпадает с утверждением — proof term отвергается, агент корректирует и пробует снова. Вам показывается доказательство на естественном языке только после прохождения верификации.

Агент может не решить задачу и скажет об этом. Но если отмечено «верифицировано» — proof term прошёл kernel, и утверждение математически истинно в рамках аксиоматики CIC + три аксиомы выше.

Mathlib

Агент работает поверх Mathlib — крупнейшей библиотеки формализованной математики:

1. ~1 500 000 строк кода на Lean 4
2. ~200 000 формализованных теорем и лемм
3. 500+ активных контрибьюторов
4. Области: алгебра (группы, кольца, поля, модули, алгебры Ли), анализ (мера Лебега, интегрирование, дифференцирование), топология (компактность, связность, гомотопия, накрывающие пространства), теория чисел, теория категорий, комбинаторика

Каждая лемма Mathlib прошла верификацию ядром Lean. Ссылка на результат из Mathlib — это ссылка на формально доказанный факт.

Границы

Единственный теоретический вектор ошибки — баг в ядре Lean (~5 000 строк, проверенных сообществом более 10 лет). На практике таких багов не обнаружено. Для сравнения: языковая модель содержит ~10¹¹ параметров, и ни один из них не проверен формально.

MathProver может не решить задачу. Может предложить неоптимальное доказательство. Но если доказательство верифицировано — оно корректно. Это гарантия by design, не by testing.

Lean 4 v4.28.0 (Leonardo de Moura, Lean FRO). Mathlib v4.28.0 (leanprover-community). Верификация: CIC + propext + Quot.sound + Classical.choice. MathProver использует Lean LSP для интерактивной формализации.