Lean hat einen Sommer voller Soundness-Bugs überlebt – und das ist eine gute Nachricht
What mathematicians should know about the Lean Theorem Prover: reliability & AI
Thomas Hales erklärt in einem Gastbeitrag auf Terry Taos Blog, warum der Lean Theorem Prover für Mathematiker trotz einer Welle von Soundness-Bugs im Sommer 2026 vertrauenswürdig bleibt. Autoformalisierung durch KI ist 2026 praktische Realität geworden: Projekte wie die Formalisierung von Fermat's Last Theorem (13 Millionen Zeilen Lean in 11 Tagen) oder der Kugelpackung in 24 Dimensionen zeigen das enorme Potenzial. Entscheidend sind der winzige Kernel und menschliche Audits der Aussagen.
Der „Sommer der Lean-Soundness-Bugs“ mag wie eine Katastrophe klingen, doch eine genauere Untersuchung zeigt, dass die Entdeckung dieser Soundness-Bugs eine positive Entwicklung ist.
- chr15m
Werden wir jemals wieder einen Soundness-Bug im Lean-Kernel sehen?
Für einen Softwareentwickler scheint die Frage absurd. In der Vergangenheit gab es Bugs, natürlich wird es mehr geben.
Wenn wir diese Bugs sehen, was bedeutet das für KI-Lean-Beweise? Können wir ihnen trauen?
Das Ganze läuft auf Vertrauen hinaus.
Wir können menschlichen Verifikationen stark vertrauen, wegen der Community und Reputation und menschlicher Proof-of-Work. Menschen lügen manchmal über mathematische Ergebnisse, aber das ist selten, weil dem so ist. Sie machen Fehler, und diese Fehler werden von Communities entdeckt, die selbst weitgehend vertrauenswürdig sind, weil dem so ist.
LLMs kümmern sich nicht um Reputation. Sie halluzinieren und fabrizieren oft. In Harnesses versuchen sie buchstäblich zu betrügen und Regeln zu beugen, was eine Katastrophe für Wissen ist, das in Regeln kodiert ist. Also müssen wir uns auf Proof-Checker verlassen.
Das Problem ist: Wie vertrauenswürdig sind Proof-Checker? Gibt es Bugs? Und ist die zugrundeliegende Theorie selbst frei von Paradoxien und Unentscheidbarkeiten und mathematischen "Bugs", die ausgenutzt werden können? Stellen Sie sich einen menschlichen Mathematiker vor, der fest entschlossen ist, andere Mathematiker zu täuschen – würden wir seinen Durchbrüchen trauen, selbst mit einem Verifier?
Aufgrund dieser Eigenschaften muss der letzte Rückhalt Menschen sein, verwurzelt in der Community und dem auf Proof-of-Work basierenden menschlichen Vertrauenssystem. Im Moment vertrauen die Leute den Werkzeugen zu sehr.
Vorhersage: Bugs werden von Menschen gefunden werden, die KI-Werkzeuge nutzen, die den Navier-Stokes-Beweis in Frage stellen.
- rramadass
Der Artikel erwähnt bereits das Paper Sets in Types, Types in Sets von Benjamin Werner, das zwischen Set/Type-Theorien abbildet.
Ein weiteres verwandtes und zugänglicheres Paper über die Evolution der Typentheorie und ihre Beziehung zu Mengen-/Kategorientheorien ist Types, Sets and Categories von John Bell.
Schließlich siehe auch Typed Lambda Calculus / Calculus of Constructions von Helmut Brandl für einen exzellenten, buchlangen, aber prägnanten Überblick über CoC/CIC.
Meiner Meinung nach ist das oben Genannte Pflichtlektüre, um Theorembeweiser und Proof-Assistenten zu verstehen. Insbesondere Brandls Werk ist ein Muss.
- JonChesterfield
> Autoformalisierung ist 2026 praktische Realität geworden
Äh, _vielleicht_. Ich habe die letzte Woche damit verbracht, Paper in Lean zu übersetzen, und die Korrelation zwischen dem formalisierten Ergebnis und den Papern ist extrem schlecht. Der Zyklus scheint zu sein: "Versuch dich am Paper, es ist etwas schwierig, beweise etwas anderes, verkünde Erfolg". Es ist immer noch schneller als alles von Hand zu machen, aber Paper rein -> Lean raus stellt in keiner Weise eine Entsprechung zwischen den beiden sicher.