In Kürze

  • Anthropic liess ein internes Forschungsmodell von Claude über elf Tage hinweg mit Dutzenden parallel arbeitenden Agenten an der Formalisierung von Fermats letztem Satz arbeiten und meldete am 4. September 2026 den ersten vollständigen, maschinell geprüften Beweis in der Beweissprache Lean.
  • Der Beweis folgt einer vereinfachten Fassung von Andrew Wiles' Originalbeweis von 1995 nach einer Darstellung von Henri Darmon, Fred Diamond und Richard Taylor, umfasst 13 Millionen Zeilen Lean-Code, beweist 29'500 Zwischen-Theoreme und gilt laut Anthropic als grösste je erstellte formale Lean-Datei.
  • Der Durchbruch gelang laut Anthropic erst, nachdem ein erster Versuch gescheitert war und das Team Claude Zugriff auf das quelloffene Werkzeug «Prove2Me» gab, das den Agenten hilft, jeweils den optimalen nächsten Beweisschritt zu bestimmen; dabei wurden nach Unternehmensangaben rund 6 Milliarden Token an Ausgabe erzeugt.

Was ist passiert?

Anthropic hat am 4. September 2026 bekanntgegeben, dass sein Sprachmodell Claude erstmals einen vollständigen, computergeprüften Beweis von Fermats letztem Satz erstellt hat. Für die Aufgabe – die sogenannte Formalisierung, also die Übersetzung eines mathematischen Beweises in eine Form, die ein Beweisassistent wie Lean automatisch verifizieren kann – setzte das Unternehmen ein internes Forschungsmodell ein, das über elf Tage hinweg mit Dutzenden parallel arbeitenden Agenten an verschiedenen Teilbeweisen arbeitete. Der resultierende Beweis folgt einer vereinfachten Fassung von Andrew Wiles' berühmtem 129-seitigem Originalbeweis aus dem Jahr 1995, orientiert an einer Darstellung von Henri Darmon, Fred Diamond und Richard Taylor, und verwendet ausschliesslich die drei Standardaxiome von Lean, ohne ausgelassene Zwischenschritte.

Das Ergebnis fällt mit 13 Millionen Zeilen Lean-Code und 29'500 bewiesenen Zwischen-Theoremen aus – nach Anthropics Angaben die grösste formale Lean-Datei, die je erstellt wurde. Ein erster Versuch, Wiles' Beweis direkt zu formalisieren, war zunächst gescheitert; den Durchbruch brachte laut Unternehmen erst der Einsatz des quelloffenen Werkzeugs «Prove2Me», das es den Agenten erleichtert, aus einer grossen Zahl möglicher nächster Beweisschritte jeweils den vielversprechendsten auszuwählen. Anthropic hat den vollständigen Beweis auf GitHub veröffentlicht.

Warum ist das wichtig?

Die Überprüfung eines komplexen mathematischen Beweises durch menschliche Fachleute kann Jahre dauern – bei Wiles' ursprünglichem Beweis von Fermats letztem Satz etwa mussten mehrere Gutachter über Monate hinweg jeden Schritt nachvollziehen, bevor er 1995 als korrekt anerkannt wurde. Eine Formalisierung in einer maschinenlesbaren Beweissprache wie Lean schafft demgegenüber Gewissheit auf Knopfdruck: Sobald ein Beweis vom Lean-Kernel akzeptiert wird, ist seine logische Korrektheit mechanisch garantiert. Dass ein KI-System eine Formalisierung, für die Fachleute bislang mehrere Jahre veranschlagt hatten, in elf Tagen erledigt, zeigt, wie stark sich Agenten-Systeme inzwischen für lang andauernde, mehrstufige Denkaufgaben eignen.

Der Fall wirft zugleich eine Frage auf, die weit über die reine Mathematik hinausreicht: Je mehr wissenschaftliche und technische Behauptungen von KI-Systemen selbst generiert werden, desto wichtiger werden unabhängige, maschinell prüfbare Nachweise ihrer Korrektheit. Formalisierungswerkzeuge wie Lean könnten damit zu einem zentralen Baustein werden, um KI-generierte Forschungsergebnisse – von Beweisen bis zu Software – überhaupt vertrauenswürdig überprüfen zu können, statt sich allein auf die Plausibilität der Ausgabe verlassen zu müssen.

Was bedeutet das für die Schweiz?

Redaktionelle Einordnung: Die folgenden Schlussfolgerungen beziehen sich auf die genannten Quellen. Sie sind keine zusätzlichen Meldungen der Originalquelle.

  • Die Schweiz zählt mit dem Lean-Ökosystem und dem international bekannten Mathlib-Projekt zu den Zentren der Formalisierungsforschung; Institute für theoretische Informatik und formale Methoden an ETH Zürich und EPFL beobachten Fortschritte wie diesen genau, weil sie zeigen, wie stark automatisiertes Theorembeweisen inzwischen als Prüfinstrument für die eigene mathematische und informatische Forschung taugt.
  • Für den Forschungsplatz Schweiz ist der immense Rechenaufwand von rund 6 Milliarden erzeugten Token bemerkenswert: Er unterstreicht, dass solche Agenten-Grossprojekte kaum ohne Zugriff auf sehr grosse Rechenkapazitäten möglich sind – ein Argument in der laufenden Debatte um den Ausbau des Swiss National Supercomputing Centre (CSCS) und der Rechenleistung für das offene Schweizer Sprachmodell Apertus.
  • Formale Verifikation mit Lean wird auch ausserhalb der reinen Mathematik genutzt, etwa zur Absicherung von Smart Contracts im Zuger «Crypto Valley» oder in sicherheitskritischer Software; ein KI-System, das komplexe Beweise in Tagen statt Jahren erstellt, könnte solche Prüfverfahren auch für Schweizer Fintech- und Sicherheitsfirmen deutlich beschleunigen.

Verwendete Quellen

Anthropic veröffentlichte die Ergebnisse am 4. September 2026 im eigenen Forschungsblog; SiliconANGLE und Techstrong.ai ordneten die Bedeutung zusätzlich ein.

Quellenstatus: 1 verlinkte Quelle · 0 von 1 Originaldaten verifiziert. Prüfregeln ansehen

  • Anthropic Anthropic Originaldatum nicht erfasst Rolle: Ausgangsquelle · Zugriff: technisch erreichbar · Abruf am 9. September 2026

Häufige Fragen

Was ist die Kernaussage zu Claude formalisiert Fermats letzten Satz: Anthropic meldet grössten je erstellten Lean-Beweis?

Anthropic liess ein internes Forschungsmodell von Claude über elf Tage hinweg mit Dutzenden parallel arbeitenden Agenten an der Formalisierung von Fermats letztem Satz arbeiten und meldete am 4. September 2026 den ersten vollständigen, maschinell geprüften Beweis in der Beweissprache Lean.

Warum ist diese KI-Meldung für die Schweiz relevant?

Die Schweiz zählt mit dem Lean-Ökosystem und dem international bekannten Mathlib-Projekt zu den Zentren der Formalisierungsforschung; Institute für theoretische Informatik und formale Methoden an ETH Zürich und EPFL beobachten Fortschritte wie diesen genau, weil sie zeigen, wie stark automatisiertes Theorembeweisen inzwischen als Prüfinstrument für die eigene mathematische und informatische Forschung taugt.

Welche Quelle nutzt KI News Schweiz für diese Einordnung?

Anthropic veröffentlichte die Ergebnisse am 4. September 2026 im eigenen Forschungsblog; SiliconANGLE und Techstrong.ai ordneten die Bedeutung zusätzlich ein.