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, bei denen es sich um spezielle Typen handelt, und Proofs (Beweise), die einfach Elemente von Propositions sind.

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 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)