Lean (Beweisassistent)

Lean ist ein mathematischer Beweisassistent und eine Programmiersprache. Lean beruht auf Calculus of constructions (nach Thierry Coquand) mit induktiven Typen. Lean ist ein Open-Source-Projekt.

Geschichte

Lean wurde hauptsächlich von Leonardo de Moura entwickelt. Lean wird von der gemeinnützigen Lean Focused Research Organization weiterentwickelt.

Mathematische Grundlagen

Aussagen in Lean werden in der Dependent type theory formuliert, einer mächtigen 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 Elemente von Propositions sind.

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

 λ x : nat => x + 5

Lean ist erweiterbar durch Lean-Scripte, die neue Axiome einführen können. Um lange Beweise zu gliedern, sind Unterziele definierbar, die in einem übergeordneten Beweis verwendet werden.

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 performanter.

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 und Kollegen formulierten die Definition perfektoider Räume und alles dafür erforderliche in Lean und als Scholze 2019 einen Beweis für einen neuen Satz vorlegte, wurde dieser in Lean formuliert und als „Liquid Tensor Experiment“ 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.

Amazon Web Services nutzt Lean, um Autorisierungsrichtlinien (authorization policies) zu verifizieren. Die Richtlinien werden in Cedar, einer Programmiersprache, formuliert. Daraus werden einerseits ausführbare formale Modelle in Lean und andererseits die Produktions-Implementierung in Rust erzeugt. Die Lean-Modelle dienen sowohl der Dokumentation als auch der Verifikation.

2026 hat ein mathematischer Laie das Erdős-Problem #1196 mit Hilfe des AI-Systems GPT-5.4 Pro gelöst. Der Beweis wurde mit Lean verifiziert.

2026 gab die Firma Anthropic bekannt, dass sie mit Hilfe von Claude-Agenten den Beweis des Satzes von Fermat in Lean geschrieben hat: 13 Millionen Zeilen Code, 29.500 Zwischentheoreme (Lemmas). Hinweis: Dieser Satz wurde schon 1995 von Andrew Wiles bewiesen. Wie in der Mathematik üblich, enthält der Beweis aber nicht jeden Folgerungsschritt (Korollar).

Ebenfalls nutzte OpenAI 2026 bei der Lösung des Navier-Stokes-Problem Lean als Verifikation.

Weblinks

• Homepage Lean Projekt
• Theorem Proving in Lean (Benutzer Dokumentation)
• Lean 4 Web zum Ausprobieren im Browser, mit einem angefangenen Beweis.