Lean-Befehle: Schnellreferenz für den Theorembeweiser

Lean ist ein interaktiver Theorembeweiser und zugleich eine funktionale Programmiersprache. Entwickelt wurde er bei Microsoft Research unter Leonardo de Moura: Projektstart 2013, die große Neuauflage Lean 4 erschien 2021 und zog auch die Mathematik-Bibliothek Mathlib auf die neue Version um. Formal basiert Lean auf dem Calculus of Inductive Constructions (CIC) — derselben Typentheorie, die auch Coq zugrunde liegt.

Wichtige Befehle

  • def — Funktion oder Konstante definieren (def quadrat (x : Nat) := x * x)
  • theorem, lemma, example — Aussagen formulieren und beweisen
  • inductive — eigenen induktiven Datentyp deklarieren
  • structure — Datensatz mit Feldern und automatischen Projektionen
  • class / instance — Typlassen und Instanzen für Überladung
  • namespace / open — Namensräume verwalten
  • import — Module laden (z.B. import Mathlib)

Taktiken und Inspektion

Beweise schreibt man in Lean mit Taktiken: intro, apply, exact, rw (rewrite), simp (Vereinfachung), cases, induction sowie calc für Gleichungsketten und omega/ring für Arithmetik. Zur Kontrolle dienen #check (Typ einer Aussage anzeigen), #eval (Ausdruck auswerten) und #print (Definition anzeigen).

Build und Ausführung

lake new meinprojekt
lake build
lean --run meinprojekt.lean

Das Build-Werkzeug lake verwaltet Projekte und Abhängigkeiten (vor allem Mathlib).

Einsatz

Lean dient der Formalisierung von Mathematik — bekannt wurde das Liquid Tensor Experiment — und der Software-Verifikation, bei der Programmeigenschaften maschinell bewiesen werden. Verwandte Werkzeuge: Coq-Befehle (gleiche Typentheorie), Idris-Befehle und Agda-Befehle (abhängige Typen).