Lean (Beweisassistent)

Lean ist ein Programm, mit dem man Mathematik in einer sehr strengen Schreibweise notiert. Der Computer liest diese Notation und kontrolliert jeden einzelnen Schritt. Stimmt eine Begründung nicht, meldet Lean einen Fehler und akzeptiert den Beweis nicht. Ein normaler Beweis in einem Fachtext ist dagegen Text für Menschen: Er enthält Sätze wie „offensichtlich gilt“ und setzt voraus, dass die Leser die Lücken selbst füllen. Lean lässt so etwas nicht zu. Alles muss auf eine kleine Zahl von Grundregeln zurückgeführt werden. Solche Programme nennt man Beweisassistenten.

Warum das wichtig ist

Mathematische Beweise sind heute oft hunderte Seiten lang. Selbst Fachleute überblicken sie kaum noch vollständig. Es ist schon vorgekommen, dass Fehler in veröffentlichten Beweisen erst nach Jahren auffielen. Ein geprüfter Lean-Beweis schließt diese Unsicherheit weitgehend aus.

Für KI ist Lean aus einem zweiten Grund interessant. Sprachmodelle, also KI-Systeme, die Texte fortschreiben, erfinden gern überzeugend klingenden Unsinn. Bei Mathematik ist das besonders heikel: Eine falsche Rechnung kann sehr sauber aussehen. Lean liefert hier ein hartes Urteil. Der Beweis geht durch oder er geht nicht durch, ohne Verhandlungsspielraum. Damit lässt sich automatisch messen, ob eine KI wirklich richtig gerechnet hat.

Wie es funktioniert

In Lean schreibt man zunächst die Behauptung hin, etwa dass es unendlich viele Primzahlen gibt. Danach folgt der Beweis als Folge von Anweisungen. Diese Anweisungen heißen Taktiken. Eine Taktik sagt zum Beispiel: „Nimm das Gegenteil an“ oder „wende diesen bereits bewiesenen Satz an“.

Der Vergleich mit einem Programmierwerkzeug trifft es gut. Wer Software schreibt, bekommt beim Übersetzen des Programms sofort Fehlermeldungen. Genauso zeigt Lean laufend an, was noch offen ist und wo eine Begründung fehlt. Man arbeitet also im Dialog mit dem Programm, statt am Ende einen fertigen Text abzuliefern.

Wichtig ist außerdem eine große Sammlung namens Mathlib. Darin haben Freiwillige über Jahre zehntausende Sätze der Schul- und Hochschulmathematik in Lean formalisiert. Wer etwas Neues beweisen will, baut auf diesem Fundament auf und muss nicht bei den Grundregeln anfangen.

Wo man dem Begriff begegnet

In den Nachrichten taucht Lean vor allem im Zusammenhang mit KI-Wettbewerben auf. Bei mathematischen Olympiade-Aufgaben treten KI-Systeme an, die ihre Lösungen in Lean abliefern. Google DeepMind hat mit AlphaProof ein solches System vorgestellt, das Olympiade-Aufgaben auf hohem Niveau löste. Auch OpenAI und mehrere chinesische Labore veröffentlichen Modelle, die Lean-Beweise erzeugen.

In der Forschung selbst nutzen Mathematiker Lean für Großprojekte. Der Fields-Medaillen-Träger Terence Tao hat mehrere eigene Ergebnisse mit Lean und vielen Mitwirkenden formalisiert. Solche Projekte laufen offen im Netz, meist auf der Plattform GitHub.

Für Schüler und Studierende ist Lean außerdem als Lernwerkzeug zugänglich. Es gibt Browser-Spiele wie das „Natural Number Game“, in denen man Schritt für Schritt einfache Beweise führt. Vorwissen im Programmieren ist dafür nicht nötig, Geduld allerdings schon.