Lean-Kernel

Lean ist ein Computerprogramm, mit dem man mathematische Beweise so aufschreibt, dass ein Rechner sie Schritt für Schritt nachprüfen kann. Der Lean-Kernel ist der innerste Teil dieses Programms. Seine einzige Aufgabe ist die Endkontrolle: Er schaut jeden Schritt eines Beweises an und prüft, ob er den festgelegten logischen Regeln folgt. Sagt er ja, gilt der Beweis als korrekt. Sagt er nein, wird der Beweis abgelehnt, egal wie überzeugend er wirkt. Entscheidend ist, dass dieser Kern absichtlich sehr klein ist: nur einige Tausend Zeilen Programmcode, während das übrige Lean-System ein Vielfaches davon umfasst.

Warum ein winziger Prüfkern so viel Vertrauen schafft

Jedes große Programm enthält Fehler. Bei einem Beweisprüfer wäre ein Fehler besonders schlimm, denn er könnte einen falschen Beweis durchwinken. Die Lösung nennt man das De-Bruijn-Prinzip: Man schiebt alles Komplizierte nach außen und lässt am Ende nur einen kleinen, gut überschaubaren Kern entscheiden. Diesen Kern können Fachleute Zeile für Zeile lesen und mehrfach unabhängig nachbauen.

Praktisch heißt das: Die bequemen Hilfsmittel von Lean dürfen Fehler haben. Solche Hilfsmittel schlagen Beweisschritte vor, ordnen Formeln um oder erledigen Routinearbeit automatisch. Wenn eines davon Unsinn produziert, fällt das spätestens beim Kern auf. Man muss also nicht dem ganzen Werkzeugkasten vertrauen, sondern nur dem Türsteher am Ende.

Genau das macht den Kern für die KI-Debatte wichtig. Ein Sprachmodell kann Behauptungen erfinden, die plausibel klingen und trotzdem falsch sind. Für diese Art Fehler gibt es den Begriff Halluzination. Ein Beweis, den der Lean-Kernel akzeptiert hat, ist dagegen nicht Ansichtssache. Hier hört das Schätzen auf und es beginnt eine harte Prüfung.

Was der Kern eigentlich nachrechnet

Lean beruht auf einer Idee, die Beweise und Programme gleichsetzt. Eine mathematische Aussage wird als Typ dargestellt, also als eine Art Bauplan oder Anforderung. Ein Beweis dieser Aussage ist dann ein Objekt, das genau diesem Bauplan entspricht. Prüfen heißt deshalb: passt das eingereichte Objekt zum verlangten Typ? Diese Frage nennt man Typprüfung, und sie ist die Kernaufgabe des Kernels.

Man kann sich das wie eine Zollkontrolle vorstellen. Der Beweis ist ein Paket mit Aufschrift, die Aufschrift ist die Aussage. Der Kern öffnet das Paket und vergleicht Inhalt mit Aufschrift, ohne sich auf Zusagen des Absenders zu verlassen. Dabei arbeitet er nur mit wenigen Grundregeln, aus denen sich alles Weitere ableiten lässt.

Der fertige Beweis, den der Kern sieht, ist meist riesig und für Menschen kaum lesbar. Was ein Mensch in Lean schreibt, sind kurze Anweisungen, sogenannte Taktiken. Diese Taktiken erzeugen im Hintergrund den vollständigen, ausführlichen Beweis. Der Kern liest nur dieses ausführliche Endergebnis. Ein häufiger Irrtum ist, der Kern würde Beweise finden. Er findet nichts, er urteilt nur.

Von der Mathematik-Community bis zu Googles Wettbewerbs-KI

Um Lean ist eine große Bibliothek gewachsen, Mathlib genannt. Dort haben Freiwillige weit über hunderttausend Sätze und Definitionen formalisiert, von Schulstoff bis zu aktueller Forschung. Bekannte Mathematiker wie Terence Tao haben eigene Ergebnisse in Lean nachgeprüft, teils um Fehler in veröffentlichten Arbeiten auszuschließen.

In den Tech-News taucht der Begriff vor allem im Zusammenhang mit KI-Systemen auf, die Mathematikaufgaben lösen. Programme wie AlphaProof von Google DeepMind schreiben ihre Lösungen direkt in Lean. Der Kernel entscheidet dann, ob eine Lösung zählt. Das ergibt ein Trainingssignal, das nicht diskutierbar ist: bestanden oder nicht bestanden. Solche Rückmeldungen sind der Grund, warum Beweisprüfer für das Training von KI-Modellen so attraktiv sind.

Lean ist dabei nicht allein. Ältere Systeme wie Coq oder Isabelle folgen demselben Grundgedanken eines kleinen, vertrauenswürdigen Kerns. Wer die Idee einmal verstanden hat, erkennt sie auch außerhalb der Mathematik wieder, etwa bei der Prüfung sicherheitskritischer Software in Flugzeugen oder Chips.