Lean Beweisassistent und KI: Wie Beweise maschinell prüfbar werden

Kategorien: Künstliche Intelligenz

Elf Tage, ein Schwarm von Agenten, 13 Millionen Zeilen Code: Eine KI hat den Beweis zu Fermats letztem Satz maschinell überprüfbar gemacht. Entscheidend war weniger die Rechenkraft als ein Prüfer, der keinen Fehler durchlässt.

Um 1637 notierte Pierre de Fermat eine Behauptung an den Rand eines Buches, für die er angeblich einen Beweis besaß. Gefunden wurde er nie. Es dauerte bis 1995, bis Andrew Wiles einen vollständigen Beweis veröffentlichte. Am 4. September 2026 meldete Anthropic nun, dass ein Schwarm von Claude-Agenten diesen Beweis in der Beweissprache Lean vollständig formalisiert hat. Möglich wurde das durch den Lean Beweisassistenten, der jeden Schritt eines Beweises maschinell prüft.

Der Beitrag ordnet diese Meldung ein. Er erklärt, was ein Beweisassistent ist und warum ein Ergebnis aus Lean als verlässlich gilt. Er beschreibt, wie die Agenten zusammenarbeiteten, und stellt die Meldung in eine Reihe mit Olympiade-Aufgaben und Erdős-Problemen. Dabei werden belegte Zahlen, Herstellerangaben und offene Fragen getrennt. Die These: Neu ist nicht allein, dass eine KI mathematisch arbeitet. Neu ist die Kombination aus einem Modell, das frei probieren darf, und einem Programm, das jeden Schritt unbestechlich abnimmt.

Fermats letzter Satz: Was Anthropic tatsächlich gemeldet hat

Der Satz besagt, dass die Gleichung aⁿ + bⁿ = cⁿ für ganze Zahlen größer als null und einen Exponenten n größer als 2 keine Lösung hat. Die Aussage ist leicht zu verstehen und war über Jahrhunderte extrem schwer zu beweisen. 1908 wurde ein Preis von 100.000 Goldmark ausgesetzt, und laut Anthropic gingen im ersten Jahr 621 falsche Beweise ein. Wiles trug 1993 einen Beweis vor, fand eine Lücke und schloss sie gemeinsam mit Richard Taylor. Die Veröffentlichung folgte im Mai 1995.

Die jüngste Meldung betrifft die Frage, wie sicher dieser Beweis ist, wenn jeder Schritt von einer Maschine geprüft wird. Die zentralen Angaben aus der Veröffentlichung von Anthropic stehen in der Tabelle.

Ein Token ist dabei ein kleiner Textbaustein, den ein Sprachmodell erzeugt, etwa ein Wortteil. Geldkosten nennt die Quelle nicht. Alle Angaben stammen vom Hersteller und sind in dieser Form nicht unabhängig nachgezählt.

Wichtig ist die Abgrenzung. Es handelt sich um eine Formalisierung, nicht um einen neuen Beweis. Der Satz war seit 1995 bewiesen. Die Agenten bauten laut Anthropic auf einer vereinfachten Fassung des Wiles-Beweises von Darmon, Diamond und Taylor auf und übernahmen Teile aus dem Formalisierungsprojekt des Imperial College und dem Projekt flt-regular. Wer von einer KI-Lösung des Fermatschen Satzes liest, sollte also nicht an eine neue mathematische Entdeckung denken, sondern an eine Verifikation. Anthropic grenzt das Ergebnis ausdrücklich von der KI-Arbeit zur Riemann-Hypothese ab, bei der Neues entdeckt worden sei.

Was ist Lean? Ein Beweisassistent, der keinen Schritt auslässt

Der Lean Beweisassistent ist eine quelloffene Programmiersprache, mit der sich mathematische Beweise so aufschreiben lassen, dass ein Computer sie prüfen kann. Die Projektseite lean-lang.org beschreibt Lean als Programmiersprache und Beweisassistent mit einem minimalen, vertrauenswürdigen Kern, der die Korrektheit sichert. Entwickelt wurde Lean von Leonardo de Moura und 2013 als Open Source veröffentlicht, wie die Simons Foundation berichtet. Seit 2023 arbeitet die gemeinnützige Lean FRO an der Weiterentwicklung, unterstützt unter anderem mit 5 Millionen US-Dollar der Simons Foundation International.

Das Prinzip lässt sich in Alltagssprache fassen. Ein Beweis in Lean ist ein Programm. Der Kern von Lean prüft Schritt für Schritt, ob jede Folgerung aus den Axiomen und aus bereits geprüften Sätzen folgt. Axiome sind die Grundannahmen der Mathematik, die ohne Beweis gelten. Ein Schritt, der nicht folgt, wird abgelehnt, ganz gleich, wie überzeugend er klingt. Wo noch ein Beweis fehlt, steht in Lean der Platzhalter „sorry“. Ein Beweis mit solchen Platzhaltern gilt als unvollständig.

Genau das macht Lean für KI-Modelle so nützlich. Sprachmodelle können überzeugend formulieren und dabei Fehler machen. In der Mathematik ist das ein Problem, denn ein Fehler in Schritt 400 kann alles danach entwerten. Mit einem Beweisassistenten wie Lean entfällt die Frage, ob dem Modell zu glauben ist.

Eine menschliche Begutachtung funktioniert anders. Fachleute lesen einen Beweis, halten ihn für plausibel und vertrauen auf ihre Erfahrung. Das ist wertvoll, kostet aber Zeit und lässt Raum für Übersehenes. Schon 2021 validierte ein Gemeinschaftsprojekt in Lean einen komplexen Beweis von Peter Scholze, wie die Simons Foundation schildert. Die Prüfung durch den Beweisassistenten ersetzt nicht das mathematische Verständnis, sie liefert aber Gewissheit über die Korrektheit.

Der Ablauf in Abbildung 1 zeigt die Arbeitsteilung: Das Modell macht Vorschläge, der Lean-Kern urteilt. Ob ein Vorschlag aus einem Menschen, einem Modell oder einem Zufallsgenerator stammt, spielt für das Urteil keine Rolle.

Mathlib und die Frage, wer prüft, was geprüft wurde

Lean allein enthält noch keine Mathematik. Die steckt in Mathlib, der gemeinschaftlich entwickelten Bibliothek, auf der fast alle Formalisierungen aufbauen. Die Lean-Seite nennt mehr als eine Million Zeilen. Die Statistikseite der Community wies beim Abruf 139.391 Definitionen, 290.502 Theoreme und 772 Beitragende aus. Wer in Lean etwas beweist, kann auf diese geprüften Bausteine zurückgreifen, statt bei null zu beginnen.

Zum Vergleich: Der Fermat-Beweis hat laut Anthropic rund 13 Millionen Zeilen und ist damit mehr als fünfmal so groß wie Mathlib. Das klingt nach einem riesigen Neubau, zeigt aber auch, wie viel formale Verifikation bei tiefen Sätzen kostet, selbst wenn Mathlib die Grundlage liefert. Der Beweis hängt von dem ab, was bereits in Mathlib formalisiert ist.

Zwei Prüffragen sind getrennt zu stellen. Erstens: Ist der Beweis korrekt? Das beantwortet Lean. Anthropic gibt an, dass nur die drei Standardaxiome verwendet werden. Zweitens: Wurde tatsächlich der Fermatsche Satz bewiesen und nicht eine abgewandelte Aussage? Hier kam ein Comparator-Werkzeug zum Einsatz, das bestätigte, dass die formalisierte Aussage mit der Formulierung in Mathlib übereinstimmt. Diese Trennung ist entscheidend. Ein fehlerfreier Beweis einer falschen Aussage wäre wertlos.

Der vollständige Beweis liegt laut Anthropic samt schriftlicher Erläuterung auf GitHub und lässt sich dort einsehen. Nicht öffentlich ist nur das verwendete Modell.

Kevin Buzzard vom Imperial College London, der das Formalisierungsprojekt seit 2024 leitet, prüfte den Beweis. Laut Anthropic hält er fest, dass der Satz ohne Annahmen außer den Axiomen der Mathematik bewiesen wird. Eine Grenze bleibt: Lean prüft Korrektheit, nicht Bedeutung. Ob ein Ergebnis interessant, elegant oder wichtig ist, beurteilt das Werkzeug nicht. Die Simons Foundation gibt entsprechende Einschätzungen von Alex Kontorovich wieder.

Agentische KI: Warum der Schwarm funktionierte

Mehrere Dutzend Agenten arbeiteten parallel. Ein Agent ist in diesem Zusammenhang ein Sprachmodell, das nicht nur antwortet, sondern selbstständig Werkzeuge nutzt, Dateien bearbeitet und Zwischenergebnisse prüft. Das Multi-Agenten-Gerüst basierte auf Claude Code. Die Agenten definierten Begriffe, bewiesen Zwischensätze und verwendeten sie für schwierigere Aussagen. Eine allgemeine Einführung bietet der Beitrag Das Zeitalter der KI-Agenten.

Den Durchbruch brachte nach Angaben von Anthropic nicht ein stärkeres Modell, sondern eine bessere Organisation. Die Plattform Prove2Me, eine offene Kollaborationsplattform von Tianyi Peng und Kolleginnen und Kollegen der Columbia University, bot drei Eigenschaften:

• Ein gerichteter azyklischer Graph der Theoremaussagen gab Orientierung: Jede Aussage zeigt, wovon sie abhängt, und es gibt keine Kreise.
• Aussagen und Beweise lagen in getrennten Dateien. Das beschleunigt die Lean-Kompilierung, weil nicht bei jeder Änderung alles neu geprüft werden muss.
• Bereits bewiesene Sätze ließen sich über natürlichsprachige Beschreibungen suchen und wiederverwenden.

Frühere Versuche ohne diese Struktur scheiterten daran, dass die Agenten den Projektstand verloren. Aufschlussreich ist, dass diese Versuche trotzdem etwa 7 Prozent der nicht-trivialen Zeilen des Endbeweises beisteuerten. Die Lehre daraus: Bei großen Aufgaben schlägt Struktur die rohe Modellstärke. Wer viele Agenten einsetzt, braucht einen gemeinsamen Plan, geteilte Ablage und klare Zuständigkeiten. Dieselbe Erfahrung machen Entwickler bei jedem größeren Agenten-Projekt.

Der menschliche Anteil blieb gering, war aber nicht null. Tianyi Peng gab gelegentlich Anweisungen auf übergeordneter Ebene, etwa die Jacobi-Varietät als Schema zu priorisieren oder den Satz von Mazur zeitnah abzuschließen. Laut der zitierten Agentenausgabe meldete das System das Wurzelergebnis am 18. August um 02:00:57 UTC als bewiesen.

Von der Olympiade zu Erdős-Problemen: KI-Beweise seit 2024

Die Fermat-Meldung steht nicht allein. Seit 2024 zeigen mehrere Ergebnisse, dass KI Mathematik beweisen kann, und sie unterscheiden sich darin, ob Lean zum Einsatz kam.

Im Juli 2024 löste AlphaProof zusammen mit AlphaGeometry 2 vier von sechs Aufgaben der Internationalen Mathematik-Olympiade und erreichte 28 von 42 Punkten, Silber-Niveau. Die Goldgrenze lag bei 29 Punkten. AlphaProof beweist in Lean und löste unter anderem die schwerste Aufgabe des Wettbewerbs. Allerdings wurden die Aufgaben vorher von Hand in formale Sprache übersetzt, und die Rechenzeit betrug bis zu drei Tage je Aufgabe. Teilnehmer haben zweimal 4,5 Stunden.

Im Juli 2025 erreichte Gemini Deep Think 35 von 42 Punkten, Gold-Niveau, offiziell von den Koordinatoren der Olympiade bewertet. Das System arbeitete in natürlicher Sprache innerhalb der Zeitgrenze und ohne Lean. Das ist ein bewusster Kontrast: Auch ohne formale Prüfung wird KI stark, doch die Ergebnisse sind dann nicht maschinell verifiziert, sondern müssen von Menschen gelesen werden. Das Unternehmen Harmonic beschreibt in einer Veröffentlichung auf arXiv sein System Aristotle, das Lean-basierte Beweissuche mit informellem Schließen und einem Geometrie-Löser verbindet und laut Abstract Leistung auf Gold-Niveau bei den Aufgaben von 2025 erreicht.

Anfang 2026 rückten die Erdős-Probleme in den Blick, eine große Sammlung offener Fragen des Mathematikers Paul Erdős. Ein Beispiel ist Problem 728, dessen Beweis durch Aristotle in Lean als Ausarbeitung auf arXiv dokumentiert ist. Laut Simons Foundation löste außerdem ein 23-Jähriger Anfang 2026 mit ChatGPT und Lean das Problem 1196.

Die Einordnung fällt vorsichtig aus. Das Wiki von Terence Tao zu KI-Beiträgen bei Erdős-Problemen versteht sich ausdrücklich nicht als Benchmark. Es nennt einen Selektionsbias, weil Erfolge eher dokumentiert werden als Fehlschläge. Es weist darauf hin, dass fehlende frühere Fortschritte oft auf Unbekanntheit statt auf Schwierigkeit deuten, dass nachträglich häufig schon vorhandene Literatur auftauchte und dass ein gelöstes Problem nicht automatisch eine publikationsreife Arbeit ist. Zugleich empfiehlt das Wiki, KI-Beweise formal in Lean zu prüfen.

Das Feld der KI-Beweise in der Mathematik reicht von Wettbewerbsaufgaben über Randprobleme bis zu großen Formalisierungen. Die Entwicklung schreitet schnell voran; ob jede Meldung hält, was die Überschrift verspricht, muss einzeln geprüft werden. Genau dafür ist ein Prüfwerkzeug wie Lean gedacht.

Wie viel ist 11 Tage wert? Zeitvergleich ohne Übertreibung

Die Zahlen laden zu großen Vergleichen ein. Fermat formulierte den Satz 1637, Wiles bewies ihn 1995, das sind 358 Jahre. Das Formalisierungsprojekt am Imperial College wurde 2024 gestartet, mit einem Blueprint von 86 Seiten, und war ursprünglich auf mehrere Jahre angelegt. Die KI-Formalisierung dauerte 11 Tage.

Diese Gegenüberstellung hinkt aus mehreren Gründen:

• Die 11 Tage sind die Laufzeit eines Agentenschwarms, nicht die Rechenzeit eines einzelnen Modells.
• Der Beweis war bekannt. Die KI musste keine neue Idee finden, sondern eine vorhandene Beweisstruktur in Lean übersetzen.
• Es gab Vorarbeit: Mathlib, Material aus dem Imperial-Projekt und aus flt-regular sowie ein Blueprint.
• Der Aufwand von etwa sechs Milliarden Output-Tokens eines internen Modells ist erheblich. Geldkosten sind nicht angegeben.

Die Gleichsetzung von 11 Tagen KI-Arbeit mit Jahrhunderten menschlicher Arbeit am Problem ist deshalb nur ein rhetorischer Vergleich. Richtig ist: Eine Arbeit, die ein Gemeinschaftsprojekt über Jahre geplant hatte, wurde in wenigen Tagen im Wesentlichen fertiggestellt.

Ein Nebenexperiment lenkt den Blick auf den Alltag. Laut Anthropic formalisierten drei persönliche Claude-Max-Abonnements in drei Tagen Vinogradovs Drei-Primzahlen-Satz. Die Autoren halten gemeinschaftliche Formalisierung mit Verbraucher-Abonnements für möglich, wenn das Gerüst stimmt. Das ist eine Einschätzung der Autoren und kein unabhängig belegtes Ergebnis.

Grenzen und offene Punkte: Was die Meldung nicht zeigt

Anthropic nennt selbst Einschränkungen. Der Beweis ist vermutlich deutlich länger als nötig, denn Mathlib ist kompakter und besser geprüft. Er hängt davon ab, was in Mathlib bereits formalisiert ist. Das verwendete Modell ist ein internes, nicht öffentliches Forschungsmodell, sodass das Ergebnis nicht von außen mit denselben Mitteln wiederholt werden kann.

Weitere Punkte bleiben offen:

• Neue Mathematik wurde nicht erzeugt. Die Formalisierung erhöht die Gewissheit, nicht das Wissen.
• Ein Beweis in Lean ist nicht automatisch verständlich. 13 Millionen Zeilen liest niemand von Anfang bis Ende.
• Lean sagt nichts über die Bedeutung eines Satzes, sondern nur über seine Korrektheit.
• Wie unabhängig die Prüfung über Buzzards Einschätzung hinaus ist, geht aus der Meldung nicht hervor.

Zu weiteren Einzelmeldungen, etwa zu Verbesserungen bei der Riemann-Hypothese oder zu Autoformalisierungs-Agenten einzelner Firmen, liegen in dieser Recherche keine Primärquellen vor, die sich selbst prüfen ließen. Diese Meldungen bleiben hier deshalb ohne Zahlen. Auch Einordnungen einzelner Fachleute werden nur übernommen, wenn die Originalaussage vorliegt.

Was der Lean-Ansatz über Mathematik hinaus bedeutet

Das Muster hinter dem Fermat-Projekt ist verallgemeinerbar: freies Probieren auf der einen Seite, harte Abnahme auf der anderen. Es passt überall dort, wo ein Ergebnis maschinell prüfbar ist. Die Lean-Seite nennt als Anwendungen außerhalb der Mathematik die Verifikation von ArkLib, einer Bibliothek zu SNARKs (kompakten kryptografischen Beweisen), und von Cedar, der Autorisierungssprache von AWS. In der Softwareentwicklung ist das Prinzip bekannt: Ein Compiler und ein Testlauf nehmen ebenfalls ab, was ein Mensch oder eine KI geschrieben hat.

Für den Umgang mit KI-Ausgaben ergibt sich daraus eine Faustregel. Je besser sich ein Ergebnis automatisch prüfen lässt, desto sicherer kann ein Modell frei arbeiten. Bei Texten, Einschätzungen und Empfehlungen fehlt diese harte Abnahme meist. Dort bleibt der Mensch der Prüfer.

Dieselbe Logik gilt für Sicherheit und Datenschutz: Nachweisbare Eigenschaften zählen mehr als bloße Behauptungen. Ob eine Webseite etwa Tracker lädt oder Sicherheitsheader setzt, lässt sich automatisiert messen. Dafür bietet der Webseiten-Check von Dr. DSGVO eine Möglichkeit, und technische Sicherheitseigenschaften lassen sich mit den Security-Checksprüfen. Beide sind keine formalen Beweise im Sinne von Lean, folgen aber demselben Gedanken: messen statt glauben.

Versuche von Dr. DSGVO

Mit Hilfe von KI wurde (wahrscheinlich) der mathematische Beweis erbracht und formalisiert, dass magische Hexagone nach einer gewissen Konstruktionsregel für jedes beliebige n existieren (n = Kantenlänge eines Sechsecks in Waben).

Die gesamte KI-Rechenzeit betrug knapp 9 Stunden. Davon arbeitete das System quasi 99.9% der Zeit autonom und benötigte keine Eingaben. Der Umfang der Beweisdateien betrug 173 MB! Die Formalisierung mit Lean mitsamt Bibliotheken verbrauchte knapp 8 GB an Speicherplatz auf der Festplatte – in Zwischenschritten! Der gesamte Beweis zog sich über eine Spanne von 5 Tagen hin. Er wurde unterbrochen aufgrund von Nutzungslimits o.ä.

Demnächst wird der Beweis hier veröffentlicht. Ob er richtig ist müssen fähige Personen beurteilen, die mehr von Mathematik verstehen als der Autor, der KI benutzte 😉

Fazit: Die Revolution ist die Prüfbarkeit

Die KI hat Fermats letzten Satz nicht neu bewiesen, sondern den Beweis von Wiles in Lean vollständig formalisiert, laut Anthropic in 11 Tagen mit mehreren Dutzend parallelen Agenten. Der Erfolg beruht auf zwei Dingen: einer Organisation, die den Projektstand sichtbar hält, und dem Lean Beweisassistenten, der nur akzeptiert, was folgt.

Die Entwicklung seit 2024 zeigt, dass KI zunehmend mathematische Beweise liefert. Wie viel davon Neues ist und wie viel bekanntes Material, muss jeweils einzeln beurteilt werden, auch das Tao-Wiki mahnt dazu. Wo Lean im Spiel ist, bleibt die Korrektheit prüfbar. Das ist der eigentliche Fortschritt: nicht mehr Behauptungen, sondern maschinell geprüfte Gewissheit.