Lean

Lean
Логотип программы Lean
Тип Инструмент интерактивного доказательства теорем
Разработчики Microsoft Research и Leonardo de Moura[вд]
Написана на Си, C++ и Lean
Операционная система кроссплатформенность
Языки интерфейса английский
Дата выпуска 2013
Аппаратная платформа кроссплатформенность
Последняя версия
Репозиторий github.com/leanprover/le…
Лицензия Apache License 2.0
Сайт lean-lang.org (англ.)

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

См. также

Примечания

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

Ссылки

Content Disclaimer

Informasi ini disarikan dari Wikipedia dan disajikan kembali untuk tujuan edukasi. Konten tersedia di bawah lisensi CC BY-SA 3.0. Kami tidak bertanggung jawab atas ketidakakuratan data yang bersumber dari kontribusi publik tersebut.

  1. The information displayed on this website is sourced in part or in whole from Wikipedia and has been adapted for the purpose of restating it. We strive to provide accurate and relevant information, however:
  2. There is no guarantee of absolute accuracy. Wikipedia is an open, collaborative project that can be edited by anyone, so information is subject to change.
  3. It is not intended to constitute professional advice. The content displayed is for informational and educational purposes only. For important decisions (e.g., medical, legal, or financial), please consult a professional.
  4. Content copyright. Wikipedia is licensed under the Creative Commons Attribution-ShareAlike License (CC BY-SA). This means that content may be reused with appropriate attribution and shared under a similar license.
  5. Responsible use. Any risk arising from the use of information from this website is entirely the responsibility of the user.