Lean

Lean
Тип	Proof assistant
Разработчик	Microsoft Research
Написана на	C++
Операционная система	Cross-platform
Языки интерфейса	английский
Первый выпуск	2013 (2013)
Аппаратная платформа	кроссплатформенность
Последняя версия	v3.4.2 (18 января 2019 (2019-01-18))
Тестовая версия	v4.0.0-m5 (7 августа 2022 (2022-08-07))
Репозиторий	github.com/leanprover/le…
Читаемые форматы файлов: Lean 3 file format и Lean 4 file format
Создаваемые форматы файлов: Lean 3 file format и Lean 4 file format
Лицензия	Apache License 2.0
Сайт	leanprover.github.io

Lean — инструмент интерактивного доказательства теорем. Основан на исчислении конструкций с индуктивными типами. Имеет открытый исходный код, размещенный на GitHub. Проект Lean был запущен Леонардо де Моурой в Microsoft Research в 2013 году.

Lean имеет интерфейс, который отличает его от других интерактивных средств доказательства теорем. Lean может быть скомпилирован на JavaScript и доступен в веб-браузере. Он имеет встроенную поддержку символов Юникода. (Они могут быть набраны с использованием последовательностей, подобных применяемым в системе LaTeX, таких как "\times" для "×".) Lean также имеет обширную поддержку метапрограммирования.

Применение

Lean привлек внимание математиков Томаса Хейлза и Кевина Базарда. Хейлз использует его для своего проекта «formalabstracts». Базард использует его для проекта Xena Одна из целей проекта Xena — переписать все теоремы и доказательства в учебной программе по математике для студентов Имперского колледжа Лондона.

В рамках проекта Xena формализовано сложное доказательство из области condensed mathematics, развиваемой Петером Шольце.

Примеры кода

Определение натуральных чисел:

inductive nat : Type
| zero : nat
| succ : nat → nat

Определение операции сложения для натуральных чисел:

definition add : nat → nat → nat
| n zero     := n
| n (succ m) := succ(add n m)

Пример простого доказательства.

theorem and_swap : p ∧ q → q ∧ p :=
    assume h1 : p ∧ q,
    ⟨h1.right, h1.left⟩

Это же доказательство:

theorem and_swap (p q : Prop) : p ∧ q → q ∧ p :=
begin
    assume h : (p ∧ q), -- assume p ∧ q is true
    cases h, -- extract the individual propositions from the conjunction
    split, -- split the goal conjunction into two cases: prove p and prove q separately
    repeat { assumption }
end

См. также

• Инструмент интерактивного доказательства теорем

Ссылки

• Lean Website
• The Natural Number Game- An interactive tutorial to learn lean