Lean (Beweisassistent)

Lean ist ein mathematischer Beweisassistent und eine Programmiersprache. Lean beruht auf Calculus of constructions (Calculus of Constructions (nach Coquand)) und Inductive type (Induktiver Typ). Lean wurde hauptsächlich von Leonardo de Moura entwickelt, als er für Microsoft Research arbeitete, bei Amazon Web Services führt er seine Entwicklung fort. Lean ist ein Open-Source-Projekt.

Hinweis: da Lean nur in englischer Sprache dokumentiert ist, werden hier die englischen Begriffe verwendet.

Mathematische Grundlagen

Aussagen in Lean werden in der Dependent type theory formuliert, eine mächtige Sprache, in der mathematische Annahmen und Folgerungen formuliert werden können. Es werden Propositions (Aussagen) definiert und Proofs (Beweise), mit denen man aus Propositions weitere Propositions folgern kann. Sowohl Propositions als auch Proofs sind Typen.

Hinweis: In der Typentheorie hat ein System induktive Typen, wenn es über die Möglichkeit verfügt, aus Konstanten und Funktionen, die Begriffe dieses Typs erzeugen, einen neuen Typ zu erstellen.

Formulierungen in Lean werden schnell sehr kompliziert, Lean unterstützt viele Vereinfachungen. Z. B.:

constant append : Π {α : Type u}, list α → list α → list α

kann auch einfacher

append (append (cons a nil) l1) l2

geschrieben werden.

Die „natürliche“ Schreibweise in Lean verwendet mathematische Zeichen und Symbole, z. B. die griechischen Buchstaben, es gibt für alle Zeichen eine ASCII Ersatzdarstellung, z. B. So kann ℕ (natürliche Zahlen) auch „nat“, der Funktionsoperator → (Pfeil) kann als „->“ geschrieben werden. Man kann Funktionen als „lambda abstraction“ formulieren, wie im Lambda-Kalkül, z. B.

 λ x : nat, x + 5

Lean „kennt“ viele mathematische Methoden, z. B. die Boolesche Logik, Beweis durch Widerspruch, Aussagelogik und mehr. Lean ist erweiterbar durch Lean-Scripte, die neue Axiome einführen können. Um lange Beweise gliedern zu können, könne Unterziele definiert werden, die in einem übergeordneten Beweis benutzt werden können.

Beispiele

Die natürlichen Zahlen können als inductive Type definiert werden. Jede natürliche Zahl ist entweder Null oder der Nachfolger einer anderen Zahl.

inductive Nat : Type
| zero : Nat
| succ : Nat → Nat

Addition kann man rekursiv wie folgt definieren:

def Nat.add : Nat → Nat → Nat
| n, Nat.zero   => n                      -- n + 0 = n
| n, Nat.succ m => Nat.succ (Nat.add n m) -- n + succ(m) = succ(n + m)

Ein einfacher proof in Lean:

theorem and_swap (p q : Prop) : p ∧ q → q ∧ p := by
  intro h            -- assume p ∧ q with proof h, the goal is q ∧ p
  apply And.intro    -- the goal is split into two subgoals, one is q and the other is p
  · exact h.right    -- the first subgoal is exactly the right part of h : p ∧ q
  · exact h.left     -- the second subgoal is exactly the left part of h : p ∧ q

Kürzer kann man stattdessen auch schreiben:

theorem and_swap (p q : Prop) : p ∧ q → q ∧ p :=
    fun ⟨hp, hq⟩ => ⟨hq, hp⟩

Implementierung

Lean steht kann in zwei Implementierungen zur Verfügung: als JavaScript-Version, die in einem Browser interaktiv ausgeführt werden kann und als installierbare Funktion (App), die in GitHub bereitsteht. Die interaktive Form ist zum Lernen und Testen vorgesehen, die App ist schneller.

Beispiele für den Einsatz von Lean

Der Mathematiker Peter Scholze erhielt 2018 die Fields-Medaille für seine Arbeit über perfektoide Räume. Kevin Buzzard formulierte diese Theorie in Lean und als Scholz 2019 einen Beweis für einen neuen Satz vorlegte, wurde dieser in Lean formuliert und als „Liquid Tensor Project“ abgeschlossen, mit dem Ergebnis, dass der Beweis aus Sicht von Lean korrekt ist.

Terence Tao, ebenfalls Fields-Medaillen Gewinner, nutzte 2023 Lean, um seinen Beweis für die Polynomiale Freimann-Ruzsa-Vermutung zu überprüfen. Er zerlegte den Beweis in viele Schritte und ca. 20 Helfer formulierten die einzelnen Abschnitte. In einigen Wochen wurde der Beweis in Lean überprüft und verifiziert.

Weblinks

• Homepage Lean Projekt
• Theorem Proving in Lean (Benutzer Dokumentation)