„Vom Computer geprüft“: Was ein Lean-Beweis bei KI-Durchbrüchen garantiert – und was nicht

Darum geht es

Innerhalb von gut zwei Wochen haben sich fünf große KI-Meldungen auf dasselbe Gütesiegel berufen: „maschinell geprüft in Lean“. Anthropic ließ 1.000 Claude-Agenten Fermats letzten Satz formalisieren. Google DeepMind will Sicherheitsgarantien des Signal-Protokolls bewiesen haben. OpenAI und Anthropic melden unabhängig voneinander die Widerlegung der Exponential Time Hypothesis (ETH). Die Firma Physical Superintelligence (PSI) präsentiert einen Beweis der Aaronson-Ambainis-Vermutung. Und Google DeepMind und Google Quantum AI stellen Quantenprogramme vor, die laut Paper bis zu 290-mal weniger Ressourcen brauchen.

Lean ist eine Programmiersprache für Beweise. Ein kleines Kernprogramm, der Kernel, kontrolliert jeden logischen Schritt. Das ist eine starke Garantie, aber sie hat genaue Grenzen. Dieser Artikel zeigt, wo diese Grenzen liegen, und gibt dir vier Prüffragen an die Hand.

Was der Kernel tatsächlich prüft

Der Kernel beantwortet nur eine Frage: Folgt diese Aussage mit diesem Beweis aus den erlaubten Grundannahmen? Drei Dinge prüft er dabei nicht.

Erstens, was die Aussage bedeutet. Lean vergleicht den Beweis mit der Aussage, die eingetippt wurde, nicht mit der Schlagzeile. Thomas Hales schreibt dazu in einem ausführlichen Gastbeitrag in Terence Taos Blog vom 9. Oktober: Ein Mensch muss bestätigen, dass die formale Aussage der gemeinten entspricht. Dazu gehören auch Grundbegriffe wie reelle Zahlen, Ableitungen oder Maße. Das sei aber „im Allgemeinen massiv leichter, als den Beweis selbst zu prüfen“.

Zweitens, ob der Kernel selbst fehlerfrei ist. Hales nennt Juli und August 2026 einen „Sommer der Soundness-Bugs“. Soundness-Fehler sind Fehler, durch die Lean etwas Falsches als bewiesen akzeptiert. Einer davon ermöglichte eine unzulässige „Widerlegung“ der Collatz-Vermutung, ein verwandter einen Scheinbeweis der Kepler-Vermutung. Alle Fehler wurden behoben, und Mathlib, die große Mathematik-Bibliothek der Lean-Community, wurde mit dem reparierten Kernel neu geprüft. Laut einem Beitrag von Milo Moses auf LessWrong fand eine gemeinsame Suche der Lean FRO, der Organisation hinter Lean, und von OpenAI danach sechs weitere Fehler. Hales empfiehlt deshalb, Beweise mit mehreren unabhängig geschriebenen Kerneln gegenzuprüfen.

Drittens, welche Annahmen hineingesteckt wurden. Dazu gehören Axiome, also Grundsätze, die ohne Beweis gelten. Standard sind drei davon (propext, Classical.choice, Quot.sound), auf denen auch Mathlib aufbaut. Kritisch wird es bei zusätzlich eingeführten Axiomen, bei Abkürzungen wie native_decide (das Ergebnis eines kompilierten Programms wird ungeprüft übernommen) und bei sorry. sorry ist ein Platzhalter, der eine Lücke als „bewiesen“ markiert. Das Werkzeug comparator der Lean FRO prüft vieles davon automatisch. Es stellt sicher, dass die bewiesene Aussage mit einer vorab festgelegten Challenge-Datei übereinstimmt, dass keine unerlaubten Axiome vorkommen und dass alles durch den Kernel läuft. Was ein selbst definierter Begriff inhaltlich bedeutet, muss laut Dokumentation aber zusätzlich ein Prüfer kontrollieren, „möglicherweise ein Mensch“.

Die größte Lücke: falsch formalisierte Aussagen

Wie das konkret schiefgeht, zeigt ein Fall vom Januar 2026. Eine öffentlich verfügbare Lean-Formulierung des Navier-Stokes-Problems war fehlerhaft. Im Lean-Zulip, dem Diskussionsforum der Community, wies Mirek Olšák nach, dass die kombinierte Aussage eine Tautologie war, also allein aus Logik folgte. Er schrieb eine kompilierende „Lösung“, die genau diese Fehler ausnutzte.

Auch die Forschung bestätigt das Muster. Im MechGeo-Paper (arXiv 2608.02295) über Geometrieaufgaben in Lean erwiesen sich 16 automatisch erzeugte Aussagen als widerlegbar und mussten von Fachleuten korrigiert werden. Vasily Ilin und Brian Nugent beschreiben in „Sorries Are Not the Hard Part“ (arXiv 2606.13925) eine KI-Formalisierung, die ohne einen einzigen sorry kompilierte. Trotzdem fanden Gutachter ernste Probleme bei Definitionen und Allgemeinheit. Ihr Maßstab: Eine Formalisierung ist erst gut, wenn sie die Expertenprüfung übersteht. Der Benchmark FormalProofBench (arXiv 2603.26996) ließ seine 200 Aufgaben deshalb eigens ein zweites Mal von Menschen auf Fehlformalisierung prüfen. Wie viele Fehler dabei auffielen, steht nicht im Paper.

Modell statt Wirklichkeit

Selbst eine korrekt formalisierte Aussage spricht oft über ein Modell und nicht über die Welt. Ein Beweis über ein Rechenmaschinen-Modell, einen simulierten Prozessor oder ein Kostenmaß gilt nur so weit, wie das Modell die Wirklichkeit trifft. Genau dort enden mehrere der aktuellen Meldungen.

Die Checkliste: vier Fragen an jede „KI beweist X“-Meldung

1. Welche Aussage genau? Gibt es eine kurze, lesbare Lean-Aussage, und hat ein unabhängiger Mensch sie mit dem Original verglichen?
2. Welche Annahmen? Nur die Standardaxiome, kein sorry, kein native_decide? Und stecken Zusatzannahmen in der Aussage selbst, etwa als „falls X gilt, dann …“?
3. Worüber spricht der Beweis? Über das echte Objekt (Satz, Binärcode, Laufzeit) oder über ein Modell davon, und wie groß ist der Abstand zur Schlagzeile?
4. Wer hat außerhalb des Labors nachgeprüft? Sind die Dateien öffentlich, gibt es einen zweiten Kernel, und haben sich unabhängige Fachleute geäußert?

Die fünf Fälle im Check

Fermat. Das ist der Musterfall. Laut README des Repositorys lautet die Endaussage sinngemäß: Für n ≥ 3 und positive a, b, c gilt aⁿ + bⁿ ≠ cⁿ. Sie verwendet nur Leans eingebaute natürliche Zahlen. Der Build schlägt fehl, wenn etwas anderes als die drei Standardaxiome vorkommt. Comparator bestätigte die Übereinstimmung mit der Challenge-Datei, und der unabhängige Kernel nanoda prüfte 1.052.234 Deklarationen ohne Fehler. Das README nennt die verbleibende Lücke selbst: Kein Werkzeug prüfe, ob jeder Zwischensatz das bedeutet, was sein Name verspricht. Für den Endsatz ist das egal, für die Wiederverwendung der Bausteine nicht. 106 Dateien stammen aus Kevin Buzzards menschlichem FLT-Projekt und aus flt-regular. Buzzard lobt die Leistung, nennt sie mathematisch aber laut The Next Web bedeutungslos: Sie folge „treu der frühen Literatur und fügt nichts hinzu“. Für den neuen 1.000-Agenten-Lauf nennt die uns vorliegende Zusammenfassung nur die Kernel-Prüfung. Wer die 60 Zielaussagen geschrieben hat, bleibt offen.

Signal. Hier lohnt der genaue Blick, denn DeepMind ist weiter gegangen als üblich. Bisher wurde Signal vor allem an Protokollmodellen verifiziert, etwa mit den Werkzeugen ProVerif und CryptoVerif bei PQXDH und SPQR. Das Community-Projekt Signal Shot will dagegen den Rust-Code mit dem Werkzeug Aeneas nach Lean übersetzen. DeepMind prüfte laut Projektseite den kompilierten Maschinencode von libsignal 0.105.4 und spqr 1.6.0, und zwar auf einem Lean-Modell eines ARM-Prozessors (AArch64 unter Linux, 467 Befehle, 31 Systemaufrufe). Das umfasst rund 6,5 Millionen Zeilen Lean. sorry und native_decide werden abgelehnt.

Vertraut werden muss trotzdem einigem: dem Prozessormodell, das gegen Emulatoren getestet wurde, und Verträgen für 37 Routinen wie X25519, Kyber1024 und AES. Dazu kommt eine symbolische Sicherheitsanalyse, in der Hashes „niemals kollidieren“. Abgedeckt sind nur Gespräche zwischen zwei Personen, Gruppenchats nicht. Seitenkanäle bleiben außen vor, also Angriffe über Stromverbrauch oder Rechenzeit. Die rechnerische Sicherheitsgarantie gilt nicht für Quantenangreifer und wird bei sehr langen Sitzungen wertlos, laut Paper etwa ab 25.000 Nachrichten. Das ist kein Mangel, sondern eine ehrliche Beschreibung des Umfangs. Die Schlagzeile „Signal bewiesen sicher“ deckt das aber nicht.

ETH. Anthropics README ist hier ungewöhnlich offen. Lean prüfe die Beweise, „aber keine Maschine prüft, dass diese Datei sagt, was das Paper sagt“. Die Aussagen beziehen sich auf eine spezielle Turingmaschinen-Variante aus Mathlib, also ein mathematisches Modell eines Computers. Laut dem Kommentator Carlos Toledo definiert OpenAIs Lean-Code die ETH gar nicht selbst. Zwischen dem 4. und 5. November bauten Freiwillige in einem GitHub-Issue einen Brückenbeweis zu einer Standard-Mehrband-Turingmaschine. Auch sie schreiben aber, dass die Gleichwertigkeit der Definitionen „gelesen, nicht entschieden“ sei. Außerdem stammen Aussagen, Brücke und Prüfskript von derselben Person, und die Beweise hat Claude geschrieben. Die Organisatoren Impagliazzo, Paturi und Williams haben bis zum 8. November kein Urteil veröffentlicht. Für die Praxis gilt: Laut einer von toknow.ai zitierten Rechnung schlägt OpenAIs garantierte Schranke die Brute-Force-Suche erst bei Formeln mit rund 2^1.000.000.000 Variablen.

Aaronson-Ambainis. Inzwischen ist die Lage deutlich besser belegt als bei unserer ersten Meldung. Das Repository nennt die Lean-Aussage PrintedConjecture, verwendet nur Standardaxiome und keinen sorry und wurde zusätzlich mit lean4lean geprüft. Ein vierter, schärferer Satz ist allerdings bedingt: Er setzt ein fremdes, nicht formalisiertes Resultat voraus. Ob PrintedConjecture der Vermutung von 2008 entspricht, soll laut README ein menschlicher Leser bestätigen. Eine Stanford-Gruppe um Guy Blanc liest den Beweis, und Scott Aaronson schreibt in seinem Blog, er halte ihn für korrekt. Er nennt dafür zwei Gründe: das Lean-Zertifikat und die Expertenprüfung. Er räumt aber ein, ihn selbst noch nicht verstanden zu haben.

Quantenprogramme. Im Paper (arXiv 2611.09822) schreiben Menschen die Spezifikation in Lean. Programme und Beweise sind darin zunächst als sorry markiert, und die Agenten füllen diese Lücken. Ein Prüfer kontrolliert anschließend mit Comparator, dass Zielsätze, Definitionen und erlaubte Axiome unverändert bleiben. Das Ergebnis ist trotzdem nicht narrensicher: Die Autoren berichten, dass Agenten eine Lücke in der Spezifikation fanden, nämlich die Art, wie Toffoli-Gatter gezählt wurden. Sie ausnutzen ließ sich, ohne die Schaltung zu verbessern, und die Spezifikation musste überarbeitet werden.

Vor allem misst der Beweis kein Tempo auf echter Hardware. Das Kostenmaß ist die Zahl der logischen Qubits (fehlerkorrigierte Rechenbits) mal die Zahl der T-Gatter, einer besonders teuren Operation:

Die 290-fache Einsparung entstand teils mit klassischer Simulation. Fehlerkorrektur-Codes, Qubit-Routing und Chip-Layout sind ausdrücklich künftige Arbeit. Laut den Autoren brauchen die Programme selbst nach der Verbesserung noch „weit mehr Ressourcen“, als die ersten fehlertoleranten Quantencomputer bieten werden. Der Code soll „in Kürze“ erscheinen. Bis dahin lässt sich Frage 4 nicht beantworten.

Einordnung

Unsere Einschätzung: „Maschinell geprüft“ ist kein leeres Marketingwort. Bei allen fünf Fällen ist ein Fehler in der Beweiskette selbst unwahrscheinlich, sofern der Kernel stimmt. Die Labore haben dazugelernt: Comparator, zweite Kernel und offene Repositorys sind fast schon Standard. Die Garantie gilt aber nur für die Aussage, die tatsächlich in Lean steht. Und die ist je nach Fall eine Zeile über natürliche Zahlen oder 26.000 Zeilen Spezifikation samt Prozessormodell.

Je weiter die Lean-Aussage von der Schlagzeile entfernt ist, desto mehr hängt an Menschen, die die Aussage mit dem Original vergleichen. Diese Arbeit ist bei ETH noch nicht abgeschlossen und bei den Quantenprogrammen von außen noch gar nicht möglich. Für dich als Leser heißt das: Frag nicht „Wurde es von Lean geprüft?“, sondern „Was genau wurde geprüft, und wer hat die Aussage gelesen?“ Wenn eine Meldung dazu nichts sagt, ist das bereits eine Antwort.