IMPERIAL COLLEGE LONDON / LONDON (IT BOLTWISE) – Eine KI-basierte Formalisierung hat Fermats letzten Satz (FLT) erstmals durch einen vollständig computergeprüften Beweis in Lean umgesetzt. Claude arbeitete weitgehend autonom über 11 Tage und erzeugte ein durch Lean verifizierbares Artefakt. Der Weg umfasste 13 Millionen Zeilen Lean-Code und 29.500 Zwischenresultate, bevor der Endbeweis als stimmig bestätigt wurde. Entscheidend ist dabei weniger die neue Mathematik als die maschinelle Überprüfbarkeit ganzer Beweisketten.
Die Schlagzeile wirkt wie ein mathematisches Jubiläum, aber der Kern der Nachricht liegt im Ingenieursdetail: Erstmals liegt eine End-to-End-Formalform von Fermats letztem Satz (FLT) vor, die nicht nur “nachgerechnet” wurde, sondern in einem Proof Assistant so verifiziert ist, dass die Korrektheit algorithmisch feststellbar bleibt. Der Weg dorthin führte über die Programmiersprache und Logik-Umgebung Lean: Claude schrieb den Beweis innerhalb von 11 Tagen weitgehend autonom, und das Ergebnis besteht aus einem vollständigen, computergeprüften Lean-Skript statt aus einer nur für Menschen nachvollziehbaren Argumentation. Damit verschiebt sich der Fokus der Forschung von der reinen Beweis-Idee hin zur Frage, wie man ein riesiges logisches Geflecht so ausdrückt, dass eine Maschine jeden einzelnen Schritt plausibilisieren kann.
Historisch betrachtet war die praktische Hürde bei FLT nie die Formulierung, sondern die Verifikation. Schon Andrew Wiles’ erster korrekter Beweis im Jahr 1995 galt als enorme Leistung: Er umfasste 129 Seiten und erforderte eine lange Prüfschleife, bis ein kritischer Gap geschlossen war. Noch schwieriger wird die Aufgabe, wenn man einen Beweis nicht nur für Fachleute “glaubwürdig” macht, sondern wenn ein System jedes Detail sehen will. Proof Assistants wie Lean verlangen deshalb eine vollständige Schritt-für-Schritt-Darstellung: Während menschliche Beweise oft ganze “offensichtliche” Zwischenschritte überspringen, muss Lean jedes Lemma und jeden Umformungsschritt explizit haben. Für FLT wurde die Formalisierung traditionell als Projekt mit Jahren erwartet; die neue Arbeit setzt genau hier an und nimmt die gesamte Kette unter formale Kontrolle.
Technisch beschrieben ist das Projekt deutlich mehr als ein einzelnes Modell, das ein Ergebnis ausspuckt. Laut Beschreibung entstand der Beweis über eine Mehr-Agenten-Umgebung, in der Dutzende Agenten parallel Konzepte definierten, Zwischenresultate formulierten und daraus immer schwierigere Aussagen ableiteten. Unterm Strich wurden 13 Millionen Zeilen Lean-Code verarbeitet, wobei im finalen Pfad 29.500 Zwischen-theorems verwendet wurden; während des gesamten Weges waren zusätzlich etwa 30.300 Aussagen im Prozess im Spiel. Als Grundlage diente eine vereinfachte Variante der bekannten Wiles-Strategie, und menschliche Eingaben blieben auf gelegentliche, hochrangige Steuerung reduziert. Der entscheidende Effekt war außerdem eine bessere Arbeitsorganisation: Prove2Me fungierte dabei als kollaborative Plattform, die unter anderem einen gerichteten azyklischen Graphen (DAG) der Theoremzustände verwaltet, damit Agenten gezielt als Nächstes passende Beweisschritte auswählen können.
Der Markt- und Forschungsbezug ergibt sich daraus, wie stark die Nachricht als “Risikoreduktion” gelesen werden kann. Die Quelle stellt explizit heraus, dass Neuheit hier vor allem die Verifikation ist: Anders als bei KI-Arbeiten, die neue mathematische Ergebnisse im Sinne einer Entdeckung liefern, geht es beim FLT-Fall um das automatische Prüfen einer bereits bekannten Struktur. Das ist relevant, weil das Vertrauen in mathematisches Wissen in der Praxis oft davon abhängt, wie zuverlässig ein Ergebnis verifiziert wird und wie schnell die Community Konsens findet. Wenn große Teile moderner Mathematik formalisiert werden können, könnten sich Überprüfungszyklen verkürzen und Fehler in der “common corpus”-Ebene leichter aufspüren lassen. Außerdem eröffnet sich ein neuer Mechanismus für das Qualitätsmanagement von KI-generierter Mathematik: Formalisierte Beweise lassen sich (zumindest im Rahmen der formalen Bibliothek) deutlich robuster beurteilen als reine Textbegründungen.
Gleichzeitig zeigt der Bericht, dass “Autonomie” nicht automatisch “Stabilität” bedeutet. Frühe Versuche der Agenten scheiterten zunächst daran, den Projektzustand konsistent zu behalten; die Beschreibung nennt gescheiterte Teilversuche, die rund 7% der nicht-boilerplate Zeilen im Endresultat ausmachen. Erfolgreich wurde das Projekt, als die Arbeitsweise um Prove2Me und einen Lean-Compilation-Ansatz ergänzt wurde, der die Ressourcen schont: Trennung von Theoremdefinition und Beweis in unterschiedliche Dateien, deren Verbindungen unabhängig gepflegt werden. Die Plattform half zudem beim Wiederverwenden: Durch eine natürlichsprachige Beschreibung jeder Theorem-Aussage sollte die Suche nach passenden Zwischenzielen weniger mühselig werden, was in großen formalen Bibliotheken wie Mathlib ein echter Engpass ist. Genau hier liegt ein praktischer Unterschied zu klassischen “Tooling”-Ansätzen: Es geht nicht nur darum, dass ein Modell rechnen kann, sondern darum, dass das System seinen Suchraum effizient organisiert.
Für die weitere Entwicklung in der Community ist der Inhalt vor allem ein Signal, dass Formalisierung skalieren kann, ohne sofort an Koordinations- und Validierungsproblemen zu zerbrechen. Die Arbeit wurde laut Beschreibung durch Lean geprüft und ein Abgleich bestätigte, dass die Aussage des FLT-Ziels mit der Formulierung aus Mathlib übereinstimmt. In der Folge wird argumentiert, dass es sinnvoll werden könnte, zu jeder menschlich lesbaren Arbeit zusätzlich einen formalisierten Beweis zu veröffentlichen, nicht als Ersatz für die didaktische Exposition, sondern als belastbares Korrektiv. Dass Anthropic zudem erwähnte, ähnliche Formalisierungsprojekte unter Beteiligung mehrerer Agenten angegangen zu haben – etwa zur Hardy-Littlewood Circle Method oder zur Vinogradov’s Three Primes Theorem – unterstreicht, dass es sich um mehr als eine einmalige Demonstration handeln soll. Unabhängig davon, ob man die Zahlen und Prozessdetails im Detail wie ein Ingenieur prüft oder sie eher als Indikator liest: Der FLT-Fall liefert eine greifbare Referenz dafür, wie sich Vertrauen in mathematische Korrektheit künftig technisch verankern lässt.
💳 Amazon-Kreditkarte mit 2.000 Euro Limit bestellen!
🔥 Heutige Hot Deals bei Amazon: Bis zu 80% Rabatte!
🎉 Amazon Haul-Store für absolute Schnäppchenjäger!
- ★ 23-stufiges KI-Go-Training – Für Spieler mit Grundkenntnissen der Regeln – Entwickelt als intelligenter Trainingspartner passt sich die KI Spielern von 18K bis 9D an. Ideal für alle, die die Grundregeln bereits beherrschen und ihr Spiel verbessern möchten.
- IHR EMOTIONALER AI-BEGLEITER: Eiliko ist mehr als nur ein Anhänger, es ist ein charismatischer KI-Freund. Mit einem dynamischen LED-Bildschirm, der eine Vielzahl von animierten Gesichtern und Ausdrucksformen anzeigt, reagiert er auf Ihre Interaktionen mit einzigartiger Persönlichkeit und Charme.
- 【MEHR LEBEN FÜR DEINEN SCHREIBTISCH】 Lerne Eilik kennen – deinen kleinen Roboter-Freund mit Persönlichkeit. Mit liebevollen Animationen, ausdrucksstarken Reaktionen und spielerischen Interaktionen bringt Eilik mehr Freude in deinen Alltag. Ob auf dem Schreibtisch, im Büro oder am Nachttisch – Eilik wird schnell zu einem vertrauten Begleiter für besondere Momente.
- 【XL-Größe für gedeihende Pflanzen】Geben Sie Ihren Pflanzen den Raum, den sie verdienen! Unser verbessertes, großes 13,7 cm großes Design bietet Platz für Pflanzen mit einem Durchmesser von bis zu 8,9 cm und damit deutlich mehr Platz für Wurzelwachstum und Pflanzengesundheit im Vergleich zu kleineren, veralteten Modellen. Die Produktabmessungen betragen 13,6 x 13,6 x 13,2 cm und das Gerät wiegt nur 355 g.
- V28 Update - JETZT MIT NEUEN FUNKTIONEN! Als Reaktion auf das Ladeproblem von Loona haben wir das automatische Aufladen 2.0 verbessert. Diese Optimierung hilft Loona, die Ladewege in verschiedenen Szenarien zu erkennen und anzupassen, um die Erfolgsquote beim automatischen Aufladen zu erhöhen. Mobile Hotspots können sich mit Loona verbinden und überwinden WLAN-Einschränkungen, sodass Sie jederzeit und überall mit Loona interagieren können.
- Die besten Bücher rund um KI & Robotik!
- Die besten KI-News kostenlos per eMail erhalten!
- Zur Startseite von IT BOLTWISE® für aktuelle KI-News!
- IT BOLTWISE® kostenlos auf Patreon unterstützen!
- Aktuelle KI-Jobs auf StepStone finden und bewerben!
- Künstliche Intelligenz: Dem Menschen überlegen – wie KI uns rettet und bedroht | Der Neurowissenschaftler, Psychiater und SPIEGEL-Bestsellerautor von »Digitale Demenz«
Du hast einen wertvollen Beitrag oder Kommentar zum Artikel "Claude liefert erste computergeprüfte Formalisierung von Fermats letztem Satz" für unsere Leser?
#Sophos
#AmazonPrime
#Bestseller
Es werden alle Kommentare moderiert!
Für eine offene Diskussion behalten wir uns vor, jeden Kommentar zu löschen, der nicht direkt auf das Thema abzielt oder nur den Zweck hat, Leser oder Autoren herabzuwürdigen.
Wir möchten, dass respektvoll miteinander kommuniziert wird, so als ob die Diskussion mit real anwesenden Personen geführt wird. Dies machen wir für den Großteil unserer Leser, der sachlich und konstruktiv über ein Thema sprechen möchte.
Du willst nichts verpassen?
Du möchtest über ähnliche News und Beiträge wie "Claude liefert erste computergeprüfte Formalisierung von Fermats letztem Satz" informiert werden? Neben der E-Mail-Benachrichtigung habt ihr auch die Möglichkeit, den Feed dieses Beitrags zu abonnieren. Wer natürlich alles lesen möchte, der sollte den RSS-Hauptfeed oder IT BOLTWISE® bei Google News wie auch bei Bing News abonnieren.
Nutze die Google-Suchmaschine für eine weitere Themenrecherche: »Claude liefert erste computergeprüfte Formalisierung von Fermats letztem Satz« bei Google Deutschland suchen, bei Bing oder Google News!