Lean — инструмент интерактивного доказательства теорем. Основан на исчислении конструкций с индуктивными типами. Имеет открытый исходный код, размещенный на GitHub. Проект Lean был запущен Леонардо де Моурой в Microsoft Research в 2013 году[2].
Lean имеет интерфейс, который отличает его от других интерактивных средств доказательства теорем. Lean может быть скомпилирован на JavaScript и доступен в веб-браузере. Он имеет встроенную поддержку символов Юникода. (Они могут быть набраны с использованием последовательностей, подобных применяемым в системе LaTeX, таких как "\times" для "".) Lean также имеет обширную поддержку метапрограммирования.
Содержание
Применение
Lean привлек внимание математиков Томаса Хейлза и Кевина Базарда.
Хейлз использует его для своего проекта «formalabstracts»[3].
Базард использует его для проекта Xena[4]
Одна из целей проекта Xena — переписать все теоремы и доказательства в учебной программе по математике для студентов Имперского колледжа Лондона.
В рамках проекта Xena формализовано сложное доказательство из области condensed mathematics[англ.], развиваемой Петером Шольце[5][6][7].
Примеры кода
Определение натуральных чисел:
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
См. также
Примечания
- Release 4.23.0 — 2025.
- Lean (неопр.). Дата обращения: 30 сентября 2021. Архивировано 18 октября 2021 года.
- Formal Abstracts (неопр.). Дата обращения: 30 сентября 2021. Архивировано 20 октября 2021 года.
- What is the Xena project? | Xena (неопр.). Дата обращения: 30 сентября 2021. Архивировано 28 сентября 2021 года.
- Kevin Hartnett. Proof Assistant Makes Jump to Big-League Math (неопр.). Quanta (28 июля 2021). Дата обращения: 1 октября 2021. Архивировано 30 сентября 2021 года.
- Davide Castelvecchi. Mathematicians welcome computer-assisted proof in ‘grand unification’ theory // Nature. — 2021. — Vol. 595. — P. 18—19. — doi:10.1038/d41586-021-01627-2.
- Completion of the Liquid Tensor Experiment (неопр.). Lean community blog (15 июля 2022). Дата обращения: 17 июля 2022. Архивировано 17 июля 2022 года.
Ссылки