Lean (Beweisassistent)

Lean ist ein quelloffener interaktiver Beweisassistent und zugleich eine funktionale Programmiersprache. Jeder Beweisschritt wird maschinell auf Korrektheit geprüft; ein akzeptierter Beweis ist im Rahmen des zugrunde liegenden Axiomensystems fehlerfrei. Lean wurde 2013 von Leonardo de Moura bei Microsoft Research begonnen und ist gegenwärtig das verbreitetste System dieser Art in der mathematischen Forschung.

Zusammenfassung

Leans Bedeutung für die KI-Debatte beruht auf einer Eigenschaft: Es liefert ein eindeutiges, maschinell prüfbares Urteil darüber, ob ein Beweis korrekt ist. Damit wird es zum Gegenstück unzuverlässiger Erzeugung – ein Sprachmodell schlägt Beweisschritte vor, Lean akzeptiert oder verwirft sie. Diese Kombination behebt genau die Schwäche, die Terence Tao als die größte der Systeme benennt: dass sie Fehler machen, die sich nicht überprüfen lassen.

Die Gemeinschaftsbibliothek mathlib umfasst über 115.000 Definitionen und 232.000 Sätze bei mehr als 1,5 Millionen Zeilen Quelltext und bildet die Grundlage, auf der neue Formalisierungen aufsetzen. De Moura formulierte das Verhältnis beider Felder 2026 zugespitzt: Formale Verifikation macht KI vertrauenswürdig, KI macht formale Verifikation wirtschaftlich.

Entwicklung

Jahr	Ereignis
2013	Beginn der Entwicklung durch Leonardo de Moura bei Microsoft Research
2017	Beginn von mathlib unter Lean 3
2018	Neuentwicklung als Lean 4 durch de Moura und Sebastian Ullrich
2020	Lean 4 übersetzt sich selbst; Scholze stellt die Formalisierungsaufgabe
Juli 2022	Liquid Tensor Experiment abgeschlossen
Sept. 2023	stabile Fassung 4.0, mathlib vollständig portiert
ab 2023	Formalisierungsprojekte unter Beteiligung von KI-Systemen

Lean 4 ist eine vollständige Neuentwicklung, in Lean selbst geschrieben. Die beiden Hauptversionen sind weitgehend unverträglich – ein Umstand mit praktischer Folge für Sprachmodelle: Da erheblich mehr Lean-3-Quelltext im Trainingsmaterial vorliegt, erzeugen Modelle bisweilen veraltete Konstruktionen.

Die Weiterentwicklung liegt seit 2023 bei der gemeinnützigen Lean Focused Research Organization (Lean FRO).

mathlib

Die Bibliothek mathlib sammelt formalisierte Mathematik und wird von einer weltweiten Gemeinschaft gepflegt. Ihr Umfang wuchs von rund 55.000 Zeilen im Jahr 2018 auf über 1,5 Millionen.

Ihre Funktion ist arbeitsökonomisch: Wer einen neuen Satz formalisiert, muss die vorausgesetzten Ergebnisse nicht erneut beweisen, sondern greift auf bereits Geprüftes zurück. Damit entsteht ein kumulativer Bestand – die Voraussetzung dafür, dass Formalisierung überhaupt Forschungsrelevanz erlangen konnte.

Bekannte Projekte

Liquid Tensor Experiment. Peter Scholze stellte 2020 die Aufgabe, ein Ergebnis aus der kondensierten Mathematik zu formalisieren, an dessen Beweis er selbst Zweifel hegte. Ein Team unter Johan Commelin schloss die Formalisierung im Juli 2022 ab und bestätigte den Beweis mit geringfügigen Korrekturen. Bemerkenswert war die Aussage der Beteiligten, sie hätten den Beweis geprüft und vereinfacht, ohne ihn vollständig zu verstehen.

Polynomiale Freiman-Ruzsa-Vermutung. Terence Tao leitete 2023/24 ein Vorhaben, das die Formalisierung binnen weniger Wochen mit verteilter Beteiligung abschloss.

Fermats letzter Satz. Kevin Buzzard leitet seit 2023 ein langfristig angelegtes Vorhaben zur Formalisierung des Wiles-Beweises.

Equational Theories. Ein von Tao angestoßenes Projekt prüfte Millionen von Implikationen zwischen algebraischen Gesetzen maschinell.

Verbindung mit KI

Die Verbindung verläuft in beide Richtungen.

Lean prüft, was KI erzeugt. Systeme wie DeepMinds AlphaProof erzeugen Beweise in Lean und lassen sie prüfen. Da die Prüfung zuverlässig ist, richtet ein fehlerhafter Vorschlag keinen Schaden an. Werkzeuge wie Lean Copilot binden Sprachmodelle unmittelbar in die Arbeitsumgebung ein.

Lean liefert Trainingssignal. Ein akzeptierter Beweis ist ein eindeutig korrektes Ergebnis. Damit eignet sich formale Mathematik für bestärkendes Lernen mit überprüfbarer Belohnung – anders als bei Präferenzurteilen entfällt die Frage, ob die Bewertung stimmt.

KI senkt die Kosten der Formalisierung. Der Aufwand, einen Beweis in Lean zu übertragen, galt lange als prohibitiv. Automatische Übersetzung natürlichsprachlicher Mathematik in formale Form verschiebt diese Rechnung. Ein Beispiel aus 2026 ist die Bibliothek Hex für rechnergestützte Algebra, deren Spezifikationen von Menschen, deren Umsetzungen und Beweise von KI-Systemen stammen.

Grenzen

Aufwand. Trotz aller Fortschritte übersteigt der Zeitbedarf für eine Formalisierung den des ursprünglichen Beweises meist erheblich.

Verstehen. Ein geprüfter Beweis ist nicht dasselbe wie ein verstandener. Das Liquid Tensor Experiment zeigte dies ausdrücklich.

Reichweite. Formalisiert ist bislang ein Ausschnitt der Mathematik. Weite Bereiche der Forschung liegen außerhalb dessen, was mathlib abdeckt.

Grundlagenvorbehalt. Ein Beweis gilt relativ zu Leans Axiomensystem und zur Korrektheit seines Prüfkerns. Dieser ist bewusst klein gehalten, um überprüfbar zu bleiben.

Quellenangaben

Avigad, Jeremy / de Moura, Leonardo / Kong, Soonho / Ullrich, Sebastian, laufend. Theorem Proving in Lean 4.
de Moura, Leonardo (2026): The Lean Theorem Prover: Design, Evolution, and Impact.
de Moura, Leonardo / Kong, Soonho / Avigad, Jeremy / van Doorn, Floris / von Raumer, Jakob (2015): The Lean Theorem Prover (System Description). In: CADE-25.
de Moura, Leonardo / Ullrich, Sebastian (2021): The Lean 4 Theorem Prover and Programming Language. In: CADE-28, LNCS 12699, S. 625–635.
Tao, Terence (2025): Machine-Assisted Proof. In: Notices of the American Mathematical Society 72 (1), S. 6–13.
The mathlib Community (2020): The Lean Mathematical Library. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs.

← Zurück zur Lexikon-Übersicht

Zuletzt bearbeitet: 10. August 2026

Zusammengestellt, formuliert, lektoriert und korrigiert mit KI-Unterstützung. Kuratiert von Nils Brauer. Alle Angaben ohne Gewähr.