Он решает головную боль с верифицированием доказательства. Вы объявляете все структуры и их свойства, пишите доказательство своего утверждения формально, и если код скомпилировался — ваша теорема / лемма / etc. доказана.
Например, объявление группы — это конкретная структура с полями и аксиомами. В Lean (и mathlib) это уже есть из коробки:
class Group (G : Type u) extends Mul G, One G, Inv G :=
(mul_assoc : ∀ a b c : G, (a * b) * c = a * (b * c))
(one_mul : ∀ a : G, 1 * a = a)
(mul_one : ∀ a : G, a * 1 = a)
(mul_left_inv : ∀ a : G, a⁻¹ * a = 1)
При этом почти всегда писать такое вручную не нужно: в mathlib уже есть готовые структуры (Semigroup, Monoid, Group, Ring, Field, и т.д.) и огромная иерархия, где все свойства автоматически подтягиваются через typeclasses. Если у типа есть
[Group G], Lean знает, что у него есть нейтральный элемент, обратные, ассоциативность и может использовать это в доказательствах без явных аргументов.Проблемы Lean 3 (предыдущая версия)
Основная боль 3 версии была не в логике (она корректна), а в автоматизации и тактиках.
Классический пример — solve_by_elim. Эта тактика пытается закрыть цель, перебирая леммы и гипотезы из контекста с бэктрекингом. Проблема в том, что порядок перебора зависел от внутреннего состояния и структуры контекста
В результате один и тот же корректный код мог:
- проходить мгновенно;
- внезапно падать по таймауту;
- зависать при малейшем изменении окружения;
Похожие вещи были и в других конструкциях: simp, repeat, комбинациях try / first, а также при разрешении метапеременных. Таймауты считались по реальному времени, из-за чего скорость машины и нагрузка влияли на результат. Это не приводило к доказательству ложных теорем, но делало валидный код хрупким, нестабильным и плохо воспроизводимым -- что для формальной математики критично.
А что сейчас
В Lean 4 это решили радикально: язык переписали на самом себе, ввели детерминированную модель исполнения (heartbeats вместо wall-clock time), переработали систему тактик и убрали неявную недетерминированность. В результате одинаковый код теперь либо всегда работает, либо всегда падает — независимо от машины и запуска.
Дока языка
Всех с наступающим или уже наступившим