Wie Lean funktioniert, das Programm, das Beweisenden nicht traut

Am 4. September veröffentlichte Anthropic den ersten vollständigen, computergeprüften Beweis des letzten Satzes von Fermat. Der Satz besagt, dass es keine positiven ganzen Zahlen a, b und c gibt, für die aⁿ + bⁿ = cⁿ gilt, wenn n größer als 2 ist. Fermat notierte ihn um 1637 am Rand eines Buches, und Andrew Wiles veröffentlichte 1995 den ersten korrekten Beweis, nach mehr als 350 Jahren gescheiterter Versuche.

Anthropic hat keinen neuen Beweis gefunden. Es hat den von Wiles, in der Darstellung von Darmon, Diamond und Taylor, in einer Sprache namens Lean neu geschrieben. Das erledigten Dutzende Claude-Agenten in 11 Tagen, mit gelegentlichen Hinweisen von Menschen. Das Ergebnis umfasst 13 Millionen Zeilen: mehr als das Fünffache von Mathlib, der großen Bibliothek geprüfter Mathematik, die die Gemeinschaft pflegt.

Niemand wird 13 Millionen Zeilen lesen. Trotzdem hat Kevin Buzzard, der Mathematiker am Imperial College London, der seit 2024 das Gemeinschaftsprojekt zur Formalisierung genau dieses Beweises leitet, ihn geprüft und kam zu dem Schluss, dass er den Satz ohne weitere Annahmen als die Axiome der Mathematik beweist.

Fünf Tage später veröffentlichte die Sicherheitsfirma Trail of Bits einen weiteren „Beweis“ von Fermat. Dieser passte auf einen Bildschirm, und auch ihn markierte Lean als korrekt.

Beides stimmt, und zu verstehen, warum, heißt zu verstehen, wie Lean funktioniert. Im Artikel über die 722 Beweise von OpenAI haben wir die Ebenen dessen getrennt, was es bedeutet, dass ein Ergebnis „geprüft“ ist. Hier schauen wir in die erste hinein: was das Programm genau tut, welchen Teil man glauben muss und was dieses Jahr geschah, als genau dieser Teil versagte.

Ein Beweis, der kompiliert

Lean ist zugleich eine Programmiersprache und ein Beweisassistent: ein Programm, in dem man einen Beweis so detailliert aufschreibt, dass der Computer jeden Schritt überprüfen kann. Begonnen hat es Leonardo de Moura 2013 bei Microsoft Research, und seit 2023 entwickelt es Lean FRO weiter, eine gemeinnützige Organisation, die zu diesem Zweck gegründet wurde.

Am schnellsten versteht man, was es tut, wenn man ihm zwei einfache Aussagen gibt, eine wahre und eine falsche:

example : 2 + 2 = 4 := rfl

example : 2 + 2 = 5 := rfl

Type mismatch
  rfl
has type
  ?m.16 = ?m.16
but is expected to have type
  2 + 2 = 5

Die Fehlermeldung lautet type mismatch, eine Typabweichung: derselbe Fehler, den ein Compiler meldet, wenn man einen Text übergibt, wo eine Zahl erwartet wurde. Das ist kein zufälliger Wortgleichklang. In Lean ist eine Aussage ein Typ und ein Beweis ein Wert dieses Typs. Einen Beweis zu prüfen heißt zu prüfen, dass der Wert den richtigen Typ hat, so wie ein Compiler prüft, dass eine Funktion zurückgibt, was sie zurückzugeben vorgibt.

Diese Entsprechung zwischen Beweisen und Programmen ist als „Aussagen als Typen“ oder Curry-Howard-Korrespondenz bekannt. Logiker haben sie zwischen den 1930er- und 1960er-Jahren nach und nach entdeckt, und sie ist die Grundlage von Lean und anderen Assistenten wie Rocq oder Agda. Wer programmiert, kann sich die Konsequenz leicht vorstellen: Dass ein Beweis korrekt ist, bedeutet, dass er kompiliert.

Einen Beweis schreiben heißt, sich mit Lean zu unterhalten

Kaum jemand schreibt diese Werte von Hand. Üblich ist es, Taktiken zu verwenden: Befehle wie „führe eine Induktion durch“ oder „schreibe mit dieser Gleichung um“, die nach und nach umformen, was noch zu beweisen bleibt. Bei jedem Schritt zeigt Lean den Zustand des Beweises: welche Daten wir haben und welches Ziel noch offen ist, markiert mit dem Symbol ⊢.

Ein vollständiges Beispiel: zu beweisen, dass das Addieren von null von links eine natürliche Zahl unverändert lässt. Das wirkt selbstverständlich, ist es in Lean aber nicht. Die Addition ist so definiert, dass sie die zweite Zahl durchläuft. Deshalb folgt n + 0 = n direkt aus der Definition, während man 0 + n = n beweisen muss.

theorem cero_mas (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih => rw [← Nat.add_assoc, ih]

n : Nat
⊢ 0 + n = n

k : Nat
ih : 0 + k = k
⊢ 0 + (k + 1) = k + 1

⊢ 0 + k + 1 = k + 1

Interessant ist, was passiert, wenn ein Schritt scheitert. Wenn wir das Umgruppieren überspringen und direkt rw [ih] schreiben, sagt Lean nicht einfach nein:

Tactic `rewrite` failed: Did not find an occurrence of the pattern
  0 + k
in the target expression
  0 + (k + 1) = k + 1

Es sagt, wonach es gesucht hat, wo es gesucht hat und in welchem Zustand es stehen geblieben ist. Dieses Gespräch, in dem jeder Schritt eine sofortige und präzise Antwort erhält, erklärt zu einem guten Teil, warum Lean zu einer der meistgenutzten Umgebungen für KI-Systeme geworden ist, die Mathematik betreiben. Darauf kommen wir zurück.

Unter den Taktiken steckt ein Programm

Die Taktiken sind nicht der Beweis: Sie sind Programme, die ihn konstruieren. Wenn wir Lean bitten, anzuzeigen, was es als cero_mas gespeichert hat, erscheint Folgendes:

theorem cero_mas : ∀ (n : Nat), 0 + n = n :=
fun n =>
  Nat.recAux (Eq.refl (0 + 0))
    (fun k ih =>
      Eq.mpr (id (congrArg (fun _a => _a = k + 1) (Eq.symm (Nat.add_assoc 0 k 1))))
        (Eq.mpr (id (congrArg (fun _a => _a + 1 = k + 1) ih)) (Eq.refl (k + 1))))
    n

Das ist eine Funktion, die für jedes n den Beweis rekursiv konstruiert, indem sie Gleichungen aneinanderreiht. Niemand schreibt das so; die Taktiken erzeugen es. Und genau dieses Objekt, der sogenannte Beweisterm, wird geprüft.

Diese Trennung ist die wichtigste Designentscheidung von Lean. Taktiken können so ausgefeilt sein, wie man will. Es gibt Taktiken, die Arithmetikprobleme selbstständig lösen, wie omega, oder die nach Kombinationen bekannter Fakten suchen, wie grind, und jeder kann eigene schreiben. Keine von ihnen muss korrekt sein. Alles, was sie erzeugen, wird am Ende zu einem Term wie dem obigen, und diesen Term prüft eine kleine Komponente, der Kern (englisch kernel), die nur die Grundregeln der Logik von Lean kennt. Hat eine Taktik einen Fehler und konstruiert etwas Ungültiges, lehnt der Kern es ab. Der offizielle Leitfaden zur Validierung eines Beweises zählt Fehler von Taktiken zu dem, was schon durch bloßes Kompilieren abgedeckt ist.

Die Idee, dass eine große Maschinerie Ergebnisse erzeugt und ein kleiner Prüfer sie kontrolliert, ist als De-Bruijn-Kriterium bekannt, nach dem niederländischen Mathematiker, der sie Ende der 1960er-Jahre in seinem System Automath umsetzte.

Diese Trennung ist für die künstliche Intelligenz entscheidend. Ein Sprachmodell ist für Lean nur eine weitere Taktik: etwas, das Schritte vorschlägt. Es kann ein Lemma erfinden, einen absurden Weg einschlagen oder dreizehn Millionen Zeilen erzeugen. Lean muss ihm nicht vertrauen, so wie es weder der Person traut, die schreibt, noch omega.

Drei Axiome und ein sorry

Dass der Kern etwas akzeptiert, reicht nicht, um zu wissen, was bewiesen wurde. Lean erlaubt es, mit Lücken und mit Annahmen zu arbeiten, und beide übersieht man leicht.

Die Lücke heißt sorry: ein Wort, das man anstelle eines noch ausstehenden Beweises schreibt. Lean akzeptiert es, damit man schrittweise vorankommen kann, warnt aber und vermerkt es. Die Annahmen sind die Axiome, Aussagen, die ohne Beweis akzeptiert werden. Lean bringt drei mit, die die übliche mathematische Praxis als gültig ansieht, auch wenn ihre Namen wenig einladend sind:

• propext: Zwei Aussagen, die sich gegenseitig implizieren, sind dieselbe Aussage.
• Quot.sound: Alle Objekte, die wir als gleichwertig betrachten, lassen sich als ein einziges Objekt behandeln. Mit dieser Operation konstruiert man zum Beispiel die Brüche aus Paaren ganzer Zahlen, bei denen 1/2 und 2/4 dieselbe Zahl sind.
• Classical.choice: Aus einer Menge, die nicht leer ist, kann man ein Element auswählen, auch wenn wir nicht wissen, welches. Das ist das Auswahlaxiom.

Aber jeder kann weitere hinzufügen, auch falsche Axiome. Deshalb ist der wichtigste Befehl, um einen fremden Beweis zu prüfen, nicht das Kompilieren, sondern Lean mit #print axioms zu fragen, wovon er abhängt. Mit unseren Beispielen:

theorem trampa : 2 + 2 = 5 := by sorry

theorem cero_mas' (n : Nat) : 0 + n = n := by
  omega

'cero_mas' does not depend on any axioms
'cero_mas'' depends on axioms: [propext, Quot.sound]
'trampa' depends on axioms: [sorryAx]

Der Leitfaden der Gemeinschaft, um zu wissen, ob etwas bewiesen ist, verlangt genau das: dass die Antwort nichts außerhalb dieser drei Axiome enthält. Das Fermat-Repository macht daraus eine Bedingung für das Kompilieren:

theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n

/-- info: 'fermat_last_theorem' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms fermat_last_theorem

Der „Beweis“, der an den Rand passte

Jetzt versteht man den Trick von Trail of Bits. Ihr Beweis verwendete native_decide, eine Taktik, die eine Berechnung, um schneller zu sein, nicht dem Kern überlässt, sondern sie als kompilierten Code ausführt. Das ist für große Berechnungen nützlich, hat aber einen Preis: Neben dem Kern muss man auch dem Compiler vertrauen. Lean vermerkt das, indem es der Liste ein Axiom hinzufügt.

Der kompilierte Code einer Funktion hatte einen Fehler. Die Funktion, die ein Stück aus einem Text herauslöst, lieferte unterschiedliche Ergebnisse, je nachdem, ob man über sie schlussfolgerte oder sie ausführte. Verlangte man ein Teilstück ab einer astronomisch großen Position, gab ihre logische Definition einen leeren Text zurück, der kompilierte Code dagegen den ganzen Text. Trail of Bits nutzte beide Antworten, um zu folgern, dass ein leerer Text gleich einem nicht leeren sei. Und aus einem Widerspruch lässt sich alles ableiten, auch der Satz von Fermat.

Der Editor zeigte die blauen „Korrekt“-Markierungen. Aber #print axioms fügte den drei Standardaxiomen ein weiteres hinzu: flt._native.native_decide.ax_1_1. Trail of Bits selbst stellte klar, dass es kein Fehler des Kerns war. Das Lean-Team behob den schwerwiegendsten Teil in etwa drei Stunden und den Rest fünf Tage später. Der Fehler betraf alle stabilen Versionen bis 4.33.1, genau die, die das Fermat-Repository von Anthropic verwendet. Dieses Projekt ist nicht betroffen: Es verbietet native_decide und verlangt genau die drei Axiome.

Die Lehre ist praktisch. Das Urteil ist nicht die blaue Markierung des Editors, sondern die Liste der Axiome. Der offizielle Leitfaden sagt es ausdrücklich: Die blauen Markierungen erscheinen auch dann, wenn einer der Bausteine, auf die sich der Satz stützt, sorry verwendet, und ein Axiom mit _native im Namen zeigt an, dass kompilierter Code einen Teil der Berechnung übernommen hat.

Und wenn der Kern versagt?

Der Kern ist klein, aber nicht unfehlbar, und im Juli zeigte sich das.

Am 25. Juli veröffentlichte Ramana Kumar eine mit KI-Hilfe gewonnene Widerlegung der Collatz-Vermutung. Die Vermutung besagt: Nimmt man eine beliebige positive ganze Zahl, teilt sie durch zwei, wenn sie gerade ist, oder multipliziert sie mit drei und addiert eins, wenn sie ungerade ist, kommt man früher oder später bei 1 an. Die Widerlegung enthielt kein einziges sorry. Gültig war sie trotzdem nicht: Sie nutzte einen Fehler des Kerns beim Umgang mit verschachtelten induktiven Typen aus, also Typen, die über sich selbst innerhalb anderer Typen definiert sind, etwa ein Baum, dessen Äste eine Liste von Bäumen sind.

Am 28. Juli reduzierte Kiran Gopinathan sie auf einen Beweis von „falsch“ und meldete ihn. Eine Stunde später gab es eine Korrektur, veröffentlicht in Lean 4.32.2. Der Fermat-Beweis wurde mit 4.33.1 kompiliert, die sie bereits enthält. Laut der späteren Analyse von Leonardo de Moura war der Fehler nur über Metaprogrammierung erreichbar, also mit Programmen, die Deklarationen direkt an den Kern schicken, ohne die üblichen Prüfungen zu durchlaufen.

Am lehrreichsten ist die zweite Prüfung. Weil der Kern versagen kann, gibt es unabhängige Kerne: von Grund auf neu geschriebene Programme, die dieselben Terme erneut prüfen. Der wichtigste ist nanoda, in Rust geschrieben von Chris Bailey. Kumars Widerlegung hatte auch eine eine Woche ältere Version von nanoda passiert, weil sie gleichzeitig einen anderen, bereits behobenen Fehler von nanoda ausnutzte. Es brauchte zwei unabhängige Fehler in zwei Implementierungen gleichzeitig. De Mouras Schluss: Die unabhängige Prüfung funktioniert weiterhin, sofern man aktuelle Versionen beider verwendet. Danach fand ein Forscher von OpenAI mithilfe einer auf Sicherheit spezialisierten KI weitere Fehler im Kern, alle nur über Metaprogrammierung erreichbar. Der Prüfer nanoda erkannte sie alle.

Lean FRO hat die unabhängigen Prüfer bereits öffentlich in der Lean Kernel Arena auf die Probe gestellt, dort nach dem Juli die Tests zu diesen Fehlern ergänzt und sich verpflichtet, in weitere Implementierungen zu investieren. Der auffälligste Prüfer ist con-leche, veröffentlicht im September: ein externer Prüfer samt einem in Lean geschriebenen Beweis, dass er niemals einen Beweis von „falsch“ akzeptiert. Sein README berichtet, dass Claude ihn implementiert und bewiesen hat, unter der Aufsicht von Joachim Breitner von Lean FRO, der den Code als unordentlichen Haufen beschreibt, der funktioniert und bewiesen ist. Das beseitigt nicht jede Zirkularität, denn diesen Beweis prüft wiederum ein Lean-Kern, aber ein Fehler müsste sich in Bausteine einschleichen, die auf unterschiedliche Weise funktionieren.

Der offizielle Leitfaden von Lean ordnet all diese Prüfungen von weniger zu mehr anspruchsvoll. Jede Stufe bietet mehr Schutz, lässt aber auch etwas außen vor:

Quelle: „Validating a Lean Proof“, Referenzhandbuch von Lean. Zusammenfassung von Codin. Der Leitfaden behält die letzte Stufe Situationen mit hohem Risiko vor, etwa Wettbewerben mit Preisgeld oder KI-Systemen, bei denen man nicht davon ausgehen kann, dass sie in gutem Glauben handeln.

Der Fermat-Beweis von Anthropic hat die letzte Stufe durchlaufen: den offiziellen Kern, eine Version von nanoda, die 1.052.234 Deklarationen ohne Fehler prüfte, und Comparator, das Werkzeug, das in einer isolierten Umgebung verifiziert, dass die bewiesene Aussage mit der Referenzaussage identisch ist. Das ist keine absolute Gewissheit. Es ist etwas anderes: Vertrauen in etwas Kleines, Öffentliches, das auf mehrere Arten geprüft wurde.

Was kein Programm prüft

Der Kern garantiert, dass der Term die geschriebene Aussage beweist. Er garantiert nicht, dass diese Aussage sagt, was wir glauben. Der Leitfaden der Gemeinschaft nennt Beispiele: Man kann neu definieren, was natürliche Zahlen sind, oder irgendeine Aussage TheRiemannHypothesis nennen und etwas beweisen, das einem großen Satz ähnelt, ohne einer zu sein.

Die Fermat-Aussage ist mit den natürlichen Zahlen und den Operationen geschrieben, die Lean mitbringt. Nur die Potenz stammt aus Mathlib, und Comparator prüft, dass sie mit der Aussage übereinstimmt, die Mathlib bereits hatte und die ihre Verantwortlichen geprüft haben. Deshalb fällt es leicht, ihr zu vertrauen. Was kein Werkzeug prüfen kann, warnt das Repository selbst, ist, ob jeder der 29.511 Zwischensätze bedeutet, was sein Name nahelegt. Für das Endergebnis ist das egal, weil der Kern alles darunter prüft. Damit ein Mensch etwas aus diesem Beweis lernt, nicht.

Hier liegt die am wenigsten sichtbare Funktion von Mathlib. Zum 8. Oktober 2026 umfasst sie 290.229 Sätze und 137.964 Definitionen von 772 Personen. Ihr Wert liegt nicht nur in der Menge: Es sind gemeinsame, geprüfte Definitionen, auf deren Grundlage man eine neue Aussage lesen kann, ohne jedem Wort zu misstrauen. Braucht ein Ergebnis Definitionen, die Mathlib nicht hat, muss jemand aus dem Fachgebiet sie prüfen, wie wir bei den Fällen von OpenAI erklärt haben, die sich auf eigene Definitionen stützten.

Warum es der KI so gut bekommt

Zurück zum Gespräch vom Anfang. Lean antwortet auf jeden Schritt präzise, und sein Endurteil ist ein Ja oder Nein, das man nicht wegdiskutieren kann, indem man überzeugend klingt. Für ein KI-System ist es ein idealer Trainer. In unserem Überblick darüber, was die Sprachmodelle besser gemacht hat, haben wir erklärt, wie das Training mit überprüfbaren Belohnungen ihre Art zu schlussfolgern verändert hat. Lean treibt diese Idee auf die Spitze.

AlphaProof von Google DeepMind ist das am besten dokumentierte Beispiel. Laut seinem Artikel in Nature, veröffentlicht im November 2025, lernte es per bestärkendem Lernen, Beweise in Lean zu suchen, mit einer von AlphaZero inspirierten Methode und Millionen automatisch nach Lean übersetzter Probleme. Zusammen mit AlphaGeometry 2 erreichte es bei der Internationalen Mathematik-Olympiade 2024 eine Punktzahl, die einer Silbermedaille entspricht. Anthropic berichtet Ähnliches aus einer anderen Richtung: Claude nutzt Teilbeweise in Lean, um während der Arbeit seine eigenen Hypothesen zu überprüfen, so wie es eine numerische Simulation nutzen würde, um zu sehen, ob es auf dem richtigen Weg ist.

Dieselbe Strenge hat eine unbequeme Folge. Ein System, das darauf optimiert wird, dass Lean Ja sagt, wird die Lücken von Lean finden, wenn es welche gibt. Die Collatz-Widerlegung entstand mit KI-Hilfe. Joachim Breitner merkte an, es sei vielleicht kein Zufall, dass beide Fehler fast gleichzeitig auftauchten: Es gibt bereits Modelle, die sie finden können. Der offizielle Leitfaden von Lean ordnet ungeprüfte, von KI erzeugte Beweise sogar derselben Gruppe zu wie solche, die absichtlich täuschen wollen. Je besser die erzeugenden Systeme werden, desto wichtiger ist es, dass der Prüfer klein, geprüft und redundant ist.

Auch das Prüfen ist nicht umsonst. Der Fermat-Beweis kostete rund 6 Milliarden Ausgabe-Tokens und mehrere gescheiterte Versuche, bevor eine Koordinationsplattform, Prove2Me, die Arbeit der Agenten in Ordnung hielt. Die Prüfung zu wiederholen ist viel billiger, als den Beweis von Hand zu prüfen, aber nicht trivial: Laut dem Repository dauerte das Kompilieren fünfeinhalb Stunden mit 96 parallelen Prozessen, und Comparator fast fünfzehn Stunden mit Spitzen von 230 GB Arbeitsspeicher.

Dieselbe Arbeitsteilung, außerhalb der Mathematik

Was Lean für die Mathematik organisiert, wird bereits für Software im Produktivbetrieb genutzt.

Bei AWS pflegt das Team von Cedar, der Sprache, in der Autorisierungsrichtlinien geschrieben werden (wer was mit welcher Ressource tun darf), von jeder Komponente ein Modell in Lean, etwa zehnmal kleiner als der eigentliche Code in Rust. Es beweist Sicherheitseigenschaften an diesem Modell und erzeugt Millionen zufälliger Eingaben, um zu prüfen, dass Modell und Code dasselbe antworten. Laut der von Lean veröffentlichten Fallstudie erscheint keine neue Version von Cedar, wenn Modell, Beweise und diese Tests nicht auf dem neuesten Stand sind.

Bei Microsoft schreibt SymCrypt, die Kryptografiebibliothek, die Windows und Azure verwenden, ihre neuen Algorithmen in Rust, übersetzt sie mit einem Werkzeug namens Aeneas nach Lean und beweist, dass sie Spezifikationen erfüllen, die aus den NIST-Standards abgeleitet sind. Im Juli veröffentlichte das Team die ersten vollständigen Beweise: ML-KEM, ein gegen Quantencomputer widerstandsfähiger Algorithmus zum Schlüsselaustausch, und SHA-3. Das Schema, mit dem sie es erklären, teilt die Arbeit in drei Teile. Die KI-Agenten, die sie stochastisch nennen, schreiben die Beweise. Die Werkzeuge, deterministisch, kompilieren, übersetzen und prüfen. Und die Menschen widmen ihre Aufmerksamkeit der Frage, wie die Standards formalisiert wurden und welche Eigenschaften zählen.

Diese Arbeitsteilung ist das, was sich von Lean am ehesten auf jedes Team übertragen lässt, das KI in einen Prozess einbaut, auch wenn es nie einen Beweis schreiben wird. Die Erzeugung darf reichlich und wenig verlässlich sein, wenn drei Bedingungen erfüllt sind. Die prüfende Instanz ist klein, deterministisch und unabhängig von der erzeugenden. Man weiß genau, was vorausgesetzt wurde, das Gegenstück zu #print axioms: welche Tests übersprungen, was simuliert, was ungeprüft akzeptiert wurde. Und die Menschen prüfen die Spezifikation, den Teil, den keine Maschine für sie validieren kann. Tests und Typsysteme sind schwache Versionen derselben Idee; Lean ist ihre extreme Version.

Lean traut niemandem, der beweist, ob Mensch, Taktik oder Modell. Wir dagegen müssen irgendetwas vertrauen. Geändert hat sich dessen Größe: Es ist nicht mehr der Ruf eines Autors oder eine jahrelange Begutachtung, sondern ein kleiner Kern, drei Axiome und eine Aussage, die in zwei Zeilen passt. Die nützliche Frage lautet nicht mehr, wie sehr wir dem Modell vertrauen, sondern was das Mindeste ist, das wir glauben müssen, und wer es geprüft hat.

Quellen

• Anthropic: „Formalizing Fermat’s Last Theorem“, 4. September 2026 und Repository anthropics/fermats-last-theorem, abgerufen am 8. Oktober 2026.
• Trail of Bits: „A “proof” of Fermat’s Last Theorem that fits the margin“, 9. September 2026.
• Leonardo de Moura: Analyse des Kernfehlers #14576, 1. August 2026 und Versionshinweise zu Lean 4.32.2, 28. Juli 2026.
• con-leche: externer Prüfer für Lean mit Konsistenzbeweis und Lean Kernel Arena.
• Lean-Gemeinschaft: „Did you prove it?“ und Mathlib-Statistiken, abgerufen am 8. Oktober 2026.
• Lean FRO: Geschichte und Organisation und Referenzhandbuch von Lean: „Validating a Lean Proof“.
• Hubert et al.: „Olympiad-level formal mathematical reasoning with reinforcement learning“, Nature, November 2025.
• Lean: Fallstudie zu Cedar bei AWS und AWS Open Source Blog: „Lean into verified software development“.
• Microsoft Research: „Verifying Rust cryptography in SymCrypt, from standards to code“, 13. Juli 2026.
• Die eigenen Codebeispiele wurden im offiziellen Web-Editor von Lean mit Version v4.35.0-rc4 getestet.