Lean: формальные доказательства и математика

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

Зачем нужен Lean

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

• формализация математических теорем и учебных курсов;
• доказательство корректности алгоритмов и структур данных;
• проверка спецификаций протоколов и моделей состояний;
• обучение логике и типам через интерактивную проверку.

Кривая входа заметная: нужно привыкнуть к tactic-режиму, зависимым типам и библиотеке Mathlib. Но обратная связь мгновенная — редактор показывает состояние цели после каждой тактики, а ошибка означает, что доказательство действительно не сходится, а не «не сошлось с ожиданием теста».

Установка

Официальный путь — VS Code с расширением Lean 4: оно само предложит установить toolchain и настроить проект. Для сервера или нестандартного окружения используйте elan, менеджер версий Lean. Он читает файл lean-toolchain в проекте и подставляет нужную версию, поэтому разные проекты не конфликтуют.

sudo apt install git curl
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
source $HOME/.elan/env
elan --version

После установки проверьте, что elan и lake доступны в PATH. Если система предлагает поставить lake через пакетный менеджер, не делайте этого: нужен именно elan, иначе версия не будет совпадать с проектом. Для работы с Mathlib также понадобится git.

Проект и Lake

Lake — штатная система сборки Lean. Шаблон math сразу добавляет зависимость от Mathlib и создаёт структуру каталогов. Первая сборка Mathlib может занять десятки минут, поэтому скачайте готовый кэш: lake exe cache get забирает olean-файлы и экономит время.

lake new myproof math
cd myproof
lake exe cache get
lake build

Файл lean-toolchain фиксирует версию Lean, а lakefile.toml или lakefile.lean — зависимости и настройки сборки. Не меняйте версию вручную без необходимости: Mathlib собирается под конкретный toolchain, и рассинхронизация даёт непонятные ошибки. Для быстрой проверки отдельного файла удобно lake env lean MyProof/Basic.lean.

Первые доказательства

В Lean утверждение — это тип, а доказательство — его элемент. Запись example не создаёт имя, а theorem создаёт. В режиме тактик после by вы последовательно преобразуете цель. Разберём простую индукцию: сумма чисел от нуля до n равна n * (n + 1) / 2, но деление лучше избежать и доказать удвоенное равенство.

import Mathlib
open scoped BigOperators

#check Nat.add_comm

example (a b : ℕ) : a + b = b + a := by
  exact Nat.add_comm a b

theorem sum_first_n (n : ℕ) :
    2 * (∑ i in Finset.range (n + 1), i) = n * (n + 1) := by
  induction n with
  | zero => simp
  | succ n ih =>
      rw [Finset.sum_range_succ, mul_add, ih]
      ring

Здесь induction разбирает два случая, simp закрывает базу, а в шаге rw переписывает сумму по диапазону и применяет предположение индукции. ring завершает тождество. Проверить, что в доказательстве нет sorry, можно командой #print axioms sum_first_n: она покажет используемые аксиомы, и sorryAx среди них быть не должно.

Тактики и поиск лемм

Mathlib огромен, и половина работы — найти нужную лемму. #check показывает тип, #print — определение или доказательство, exact? и apply? пытаются подобрать готовое решение, а simp? предлагает набор упрощений. Внешний поиск по именам и типам доступен через Loogle. Полезные приёмы для чисел и алгебры:

example (x : ℝ) : 0 ≤ x ^ 2 := by
  positivity

example (x : ℝ) (h : x ≠ 0) : x / x = 1 := by
  exact div_self h

#check Finset.sum_range_succ
#eval 2 + 2

omega решает линейную арифметику над целыми и натуральными, linarith — линейные неравенства, nlinarith добавляет нелинейные комбинации, norm_num считает конкретные числа, ring — тождества в кольцах. Не пытайтесь заменять ими понимание: если тактика не срабатывает, полезно разбить цель на промежуточные have и явно назвать нужные леммы.

Структура и проверка

Кроме тактик, Lean поддерживает обычные термины: def, structure, inductive, сопоставление с образцом. Это делает его полноценным языком для написания программ, которые можно исполнять через #eval. Для больших проектов важна дисциплина: маленькие леммы, понятные имена, отдельные файлы и сборка без предупреждений.

def double (n : ℕ) : ℕ := 2 * n

theorem double_eq_add (n : ℕ) : double n = n + n := by
  unfold double
  ring

В CI запускайте lake build и отдельно ищите sorry: предупреждение не всегда валит сборку. Полезно включить set_option autoImplicit false, чтобы не появлялись неявные переменные, и зафиксировать версию toolchain. Для независимой проверки существует чекер lean4checker, который перепроверяет окружение ядром Lean.

lake build
grep -R --include='*.lean' -n '\bsorry\b' .
lake env lean MyProof/Basic.lean
lean --version

Не храните в репозитории сгенерированные .olean и кэш сборки; в CI кэшируйте .lake и скачивайте Mathlib-кэш. Если сборка стала медленной, проверьте, не импортируется ли весь Mathlib в каждом файле: точечные импорты ускоряют проверку, хотя требуют аккуратности.

Ограничения

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

Итог

Lean 4 даёт практический путь от школьной индукции до промышленной верификации: elan и Lake ставятся за минуты, Mathlib даёт готовую математику, а ядро гарантирует, что принятое доказательство не содержит скрытых дыр. Начните с установки расширения VS Code, маленького проекта с lake new и одной теоремы об индукции. Затем добавьте #print axioms и проверку на sorry в CI — и вы получите процесс, где формальная гарантия становится частью обычной инженерной работы, а не отдельным экспериментом.