Lean — инструмент интерактивного доказательства теорем. Основан на исчислении конструкций с индуктивными типами. Имеет открытый исходный код, размещенный на GitHub. Проект Lean был запущен Леонардо де Моурой в Microsoft Research в 2013 году.
Lean имеет интерфейс, который отличает его от других интерактивных средств доказательства теорем. Lean может быть скомпилирован на JavaScript и доступен в веб-браузере. Он имеет встроенную поддержку символов Юникода. (Они могут быть набраны с использованием последовательностей, подобных применяемым в системе LaTeX, таких как "\times" для "×".) Lean также имеет обширную поддержку метапрограммирования.
Применение Lean привлек внимание математиков Томаса Хейлза и Кевина Базарда. Хейлз использует его для своего проекта «formalabstracts». Базард использует его для проекта Xena Одна из целей проекта Xena — переписать все теоремы и доказательства в учебной программе по математике для студентов Имперского колледжа Лондона.
В рамках проекта Xena формализовано сложное доказательство из области , развиваемой Петером Шольце.
Примеры кода Определение натуральных чисел: 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
Категория:Программное обеспечение с лицензией Apache Категория:Microsoft Research Категория:Свободное программное обеспечение, написанное на C++ Категория:Свободное и открытое программное обеспечение Категория:Функциональные языки программирования Категория:Типозависимые формальные языки Категория:Инструменты интерактивного доказательства теорем