Lean

Lean ist eine besondere Programmiersprache. Man schreibt darin keine Apps, sondern mathematische Beweise. Ein Beweis ist eine lückenlose Begründung dafür, dass eine Aussage stimmt — etwa, dass es unendlich viele Primzahlen gibt. Normalerweise schreiben Menschen solche Begründungen in Worten und Formeln auf. Ein anderer Mensch muss sie dann lesen und prüfen. In Lean schreibt man den Beweis so streng auf, dass ein Programm ihn prüfen kann. Fehlt ein Schritt, meldet Lean einen Fehler. Erst wenn alles passt, gilt der Beweis als bestätigt. Solche Programme nennt man Beweisassistenten.

Warum das wichtig ist

KI-Systeme, die Text erzeugen, klingen oft überzeugend und sind trotzdem falsch. Bei Mathematik fällt das besonders auf. Ein Rechenweg kann sauber aussehen und in Schritt vier einen stillen Denkfehler enthalten. Ein Mensch muss dann mühsam nachprüfen. Genau hier ist Lean nützlich.

Lean liefert ein hartes Urteil: korrekt oder nicht. Es gibt kein „fast richtig". Damit lässt sich KI-Training automatisieren. Ein Modell erzeugt Tausende Beweisversuche, Lean sortiert die falschen aus, und mit den geglückten wird weitertrainiert. Man braucht keine Fachleute, die jede Lösung von Hand bewerten. Firmen wie Google DeepMind und OpenAI haben damit Systeme gebaut, die Aufgaben auf dem Niveau von Mathematik-Olympiaden lösen.

Über die KI hinaus prüfen Mathematiker mit Lean auch eigene Arbeiten. Manche moderne Beweise sind hunderte Seiten lang, und kaum jemand kann sie vollständig kontrollieren.

Wie es funktioniert

Lean kennt eine kleine Menge Grundregeln des logischen Schließens. Jeder Beweisschritt muss aus diesen Regeln oder aus schon bewiesenen Aussagen folgen. Der Kern von Lean, der das kontrolliert, ist absichtlich klein gehalten. Je weniger Code, desto weniger Stellen für eigene Fehler.

Man kann sich das wie ein sehr strenges Brettspiel vorstellen. Es gibt eine Startstellung, das ist die Behauptung. Es gibt erlaubte Züge, das sind die Logikregeln. Der Beweis ist eine Zugfolge zum Ziel. Lean prüft nur, ob jeder Zug regelkonform war. Kreativität liefert der Mensch oder die KI.

Damit nicht jeder bei Null anfängt, gibt es Mathlib. Das ist eine gemeinsam gepflegte Sammlung von über einer Million bereits bewiesener Aussagen. Wer etwas Neues beweist, baut darauf auf. Die aktuelle Version der Sprache heißt Lean 4.

Wo man dem Begriff begegnet

Im Alltag praktisch nie — Lean ist ein Werkzeug für Forschung und Lehre. In Tech-News taucht es dagegen regelmäßig auf. Meldungen über KI-Systeme, die Mathe-Wettbewerbe gewinnen, erwähnen fast immer, dass die Lösungen in Lean formalisiert und geprüft wurden. Das ist der Punkt, der solche Ergebnisse glaubwürdig macht.

Der Begriff fällt auch bei Fachkonferenzen und in Diskussionen über verlässliche KI. Die Grundidee interessiert Anleger und Unternehmen: Wenn eine Maschine Ergebnisse automatisch überprüfen kann, lässt sich KI in Bereichen einsetzen, in denen Fehler teuer sind. Ähnliche Prüfverfahren nutzt man bereits für Software in Flugzeugen und Chips. Vorsicht bei der Suche: „Lean" heißt im Wirtschaftsdeutsch auch eine Methode zur Vermeidung von Verschwendung in der Produktion. Das hat mit dem Beweisassistenten nichts zu tun.