Lean

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

В рамках проекта Xena формализовано сложное доказательство из области condensed mathematics^[en], развиваемой Петером Шольце^[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

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

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