Lean

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

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

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

Применение

[править | править код]

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

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

Примеры кода

[править | править код]

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

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

Примечания

[править | править код]
  1. Lean. Дата обращения: 30 сентября 2021. Архивировано 18 октября 2021 года.
  2. Formal Abstracts. Дата обращения: 30 сентября 2021. Архивировано 20 октября 2021 года.
  3. What is the Xena project? | Xena. Дата обращения: 30 сентября 2021. Архивировано 28 сентября 2021 года.
  4. Kevin Hartnett. Proof Assistant Makes Jump to Big-League Math. Quanta (28 июля 2021). Дата обращения: 1 октября 2021. Архивировано 30 сентября 2021 года.
  5. 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.
  6. Completion of the Liquid Tensor Experiment. Lean community blog (15 июля 2022). Дата обращения: 17 июля 2022. Архивировано 17 июля 2022 года.