Künstliche Intelligenz
Fermats letzter Satz: KI liefert maschinell geprüften Beweis
Bewiesen ist Fermats letzter Satz seit 1995, doch nun hat das KI-Unternehmen Anthropic nach eigenen Angaben erstmals eine vollständig computerverifizierte Fassung dieses Beweises vorgelegt. Ein Schwarm von Claude-Agenten soll sie in elf Tagen im Beweisassistenten Lean geschrieben haben: 13 Millionen Zeilen Code, 29.500 Zwischentheoreme. Die Fachwelt hatte dafür Jahre veranschlagt. Der Code liegt offen, eine unabhängige Bewertung steht weitgehend aus.
Weiterlesen nach der Anzeige
Es geht hier ausdrücklich nicht um neue Mathematik. Fermats letzter Satz – die Gleichung xⁿ + yⁿ = zⁿ hat für ganzzahlige Exponenten n > 2 keine ganzzahligen Lösungen – wurde 1995 von Andrew Wiles auf 129 Seiten bewiesen und gilt in der Fachwelt seither als gesichert. Was fehlte, war die Formalisierung: die Übersetzung dieses Beweises in eine Form, die ein Computer Schritt für Schritt automatisch nachprüfen kann. Genau das soll Claude nun geleistet haben, wie Anthropic in einem Beitrag zur Formalisierung von Fermats letztem Satz schreibt.
Werkzeug der Wahl war wie schon bei früheren KI-Beweisen der Beweisautomat Lean. Dabei handelt es sich um eine Programmiersprache und ein Prüfsystem in einem. Mathematische Aussagen und ihre Herleitungen werden als Code notiert, den Lean anschließend gegen ein festes logisches Regelwerk prüft. Geht die Kette nicht lückenlos auf, kompiliert der Beweis schlicht nicht. Vertrauen muss man am Ende nur noch dem kleinen Kern des Systems und dessen Axiomen – nicht mehr der Sorgfalt einzelner Gutachter.
Der Aufwand dafür ist allerdings enorm: Ein für Menschen geschriebener Beweis überspringt viele als offensichtlich geltende Schritte und baut auf Jahrhunderten publizierter Arbeit auf. Lean muss jeden einzelnen Schritt sehen, egal wie trivial, und kann dabei nur auf den vergleichsweise winzigen Teil der Mathematik zurückgreifen, der bereits formalisiert vorliegt. Gesammelt ist dieser Bestand in Mathlib, der zentralen Community-Bibliothek formalisierter Mathematik.
Der Anthropic-Forscher Tianyi Peng, dessen Gruppe an der Columbia University Werkzeuge für KI-gestützte Formalisierung entwickelt, wollte prüfen, ob Claude beim Formalisieren von Fermats letztem Satz (Fermat’s Last Theorem, FLT) überhaupt Fortschritte macht. Das Ergebnis habe die Erwartungen übertroffen: In elf Tagen habe Claude weitgehend autonom die erste durchgängige, computergeprüfte Fassung produziert. Herausgekommen seien 13 Millionen Zeilen Lean-Code und rund 29.500 Zwischentheoreme. Dutzende Claude-Agenten hätten dabei zusammengearbeitet, um Konzepte zu definieren, Zwischentheoreme zu beweisen und damit immer schwierigere Aussagen zu belegen.
Formalisiert wurde nach diesen Angaben eine vereinfachte Fassung von Wiles’ Beweis nach Darmon, Diamond und Taylor. Menschlicher Input habe sich auf gelegentliche High-Level-Anweisungen Pengs beschränkt.
Wie belastbar ist die Formalisierung?
Weiterlesen nach der Anzeige
Nach Anthropics Darstellung wurde das Ergebnis von Lean geprüft und nutzt nur Leans drei Standardaxiome, und ein Komparator bestätigte, dass die Theorem-Aussage mit Mathlibs eigener FLT-Formulierung übereinstimmt. Der vollständige Beweis liegt samt schriftlichem Walkthrough im GitHub-Repository von Anthropic. Ob ein Lean-Beweis kompiliert, kann jeder Dritte feststellen.
Die Prüfung adaptiert Teile aus dem von Kevin Buzzard geleiteten FLT-Projekt am Imperial College London sowie aus dem flt-regular-Projekt; Lean und Mathlib gehen auf Beiträge von Hunderten Mathematikern zurück. Buzzards 2024 gestartetes Community-Projekt ist bis September 2029 gefördert; allein der Blueprint des Projekts umfasst 86 Seiten.
Buzzard hat die Arbeit begutachtet und spricht von einem großen Schritt hin zur automatischen Formalisierung der modernen mathematischen Literatur. Buzzard hat den Code inzwischen selbst kompiliert und den Komparator laufen lassen – er hält stand. Mathematisch liefere die Arbeit aber nichts Neues, die Formalisierung folge nur der frühen Literatur zum Beweis, schreibt er in seinem Blog Xena Project.
Der Weg zum Ergebnis
Interessant zu lesen ist, dass zunächst mehrere Anläufe scheiterten. Zwar hätten die ersten Agenten-Teams Teilerfolge erzielt, den Überblick über den Projektzustand aber schnell verloren und aufgehört, effektiv zusammenzuarbeiten. Der Durchbruch kam laut Anthropic erst mit dem Wechsel auf Prove2Me, eine offene Plattform zur Formalisierung von Mathematik, die Peng und Kollegen an der Columbia University entwickelt haben. Sie pflegt einen gerichteten azyklischen Graphen von Theoremaussagen, anhand dessen die Agenten entscheiden, welche Beweise sie als Nächstes angehen. Dies soll Speicherdegradation entgegenwirken und Parallelarbeit ermöglichen.
Der Erfolg hängt also erkennbar nicht am Modell allein, sondern an der unterstützenden Infrastruktur und den Steuerungsmechanismen drumherum. Das Agententeam verbrauchte laut Anthropic rund sechs Milliarden Output-Token, woraus sich Kosten zwischen 100.000 und 300.000 US-Dollar hochrechnen lassen – eine Summe nennt Anthropic selbst nicht. Dass es kleiner geht, soll ein Nebenexperiment zeigen – mit drei privaten Claude-Max-Abos formalisierten Agenten über Prove2Me in drei Tagen den Drei-Primzahlen-Satz von Winogradow.
Die Meldung reiht sich in eine Serie von KI-Erfolgen ein, deren Bilanz gemischter ist, als die Schlagzeilen nahelegen. Bereits 2024 erreichten die DeepMind-Modelle AlphaProof und AlphaGeometry 2 bei der Internationalen Mathematik-Olympiade Silbermedaillenniveau mit vier von sechs gelösten Aufgaben.
Im April 2026 löste ein 23-Jähriger mit einem einzigen Prompt an GPT-5.4 Pro ein 60 Jahre altes Erdős-Problem – bemerkenswert vor allem wegen des Lösungswegs über Markov-Ketten; auch dieser Beweis wurde in Lean formal verifiziert. Kurz darauf widerlegte ein internes OpenAI-Reasoning-Modell eine 80 Jahre alte Annahme zum „planar unit distance“-Problem – wobei die prüfenden Mathematiker anmerkten, dass sich die Argumentation entscheidend auf Ideen stütze, die zumindest im Nachhinein anderen Autoren zugeschrieben werden könnten.
Hintergrund: Warum der Satz so lange widerstand
Faszinierend an Fermats letztem Satz ist, dass er zwar einfach zu verstehen ist, der Beweis aber mehr als 350 Jahre lang auf sich warten ließ. Fermat war hauptberuflich Jurist und notierte um 1640 an den Rand eines Buches, er habe einen wunderbaren Beweis gefunden, der Rand sei aber zu schmal. Wie ernst es die Fachwelt mit der Suche meinte, zeigt der Wolfskehl-Preis: 1908 wurden 100.000 Goldmark ausgelobt, allein im ersten Jahr gingen mehr als 600 fehlerhafte Beweisversuche ein.
Andrew Wiles kam als Zehnjähriger über ein Buch zum Problem und griff es erst wieder auf, als Gerhard Frey 1986 die Verbindung zur Taniyama-Shimura-Vermutung aufzeigte. Wiles präsentierte im Juni 1993 seinen vermeintlich korrekten Beweis. Zwei Monate nach Beginn der Prüfung deckte die Rückfrage eines Gutachters eine kritische Lücke auf. Wiles brauchte ein weiteres Jahr – zuletzt mit seinem früheren Studenten Richard Taylor – und stand kurz vor dem Aufgeben, als er erkannte, dass ein zuvor verworfener Ansatz die Lösung war. Genau diese Episode ist das stärkste Argument für Formalisierung – und der Grund, warum das Vorhaben überhaupt in Angriff genommen wurde.
Lesen Sie auch
(vza)
Künstliche Intelligenz
Microsoft-Ausfall: Woran es lag und wer besonders litt
Eine stundenlange Großstörung hat weltweit Unternehmen und Verbraucher von zentralen Cloud-Angeboten des Software-Konzerns Microsoft abgeschnitten. Betroffen waren nicht nur der E-Mail-Dienst Outlook, sondern generell Dienste aus dem Cloud-Paket Microsoft 365. Beim Bürokommunikations-Angebot Teams etwa funktionierten das Planen von Besprechungen und Kalender-Anbindungen nicht richtig. Zudem waren der KI-Assistent Copilot sowie Schnittstellen zu Drittanbietern zeitweise gestört, darunter KI-Dienste wie OpenAI und Anthropic.
Weiterlesen nach der Anzeige
Microsoft machte zum Freitagnachmittag nach und nach Fortschritte – bis die Systeme dann wieder stabil liefen. Die Dienste seien zur Sicherheit schrittweise hochgefahren worden, auch wenn es dadurch länger gedauert habe. Der Konzern betonte danach, die Störung sei auf ein hausgemachtes Problem und nicht auf eine Cyberattacke oder KI-Aktivität zurückgegangen.
Der Grund habe letztlich in einem zuvor durchgeführten Upgrade der Netzwerk-Kapazität gesteckt. Ein dabei eingeführtes Problem sei erst nach jüngsten Netzwerk-Änderungen in Erscheinung getreten, hieß es. Später werde es einen ausführlichen Bericht zu dem Zwischenfall geben.
Zug- und Flugverkehr weitgehend stabil
Die Deutsche Bahn meldete wegen der Störung kaum Probleme. „Züge fahren unabhängig von Microsoft-Systemen, deshalb läuft der bundesweite Bahnbetrieb stabil“, teilte ein Sprecher des bundeseigenen Konzerns mit. In ganz wenigen Fällen sei es zu Verzögerungen gekommen, „weil kurzfristige Fahrplananpassungen nicht per E-Mail versendet werden konnten“. Bei der Lufthansa gab es nach Angaben eines Sprechers keine Auswirkungen auf den Flugverkehr. Es seien andere Systeme im Einsatz. Auch die Flughäfen in Frankfurt und Berlin teilten mit, dass die Microsoft-Probleme sich nicht auf den Flugbetrieb auswirkten.
Bei Deutschlands größtem Strom-Verteilnetzbetreiber Eon war der Betrieb der Energienetze nach eigenen Angaben nicht betroffen. Grund dafür sei eine klare Trennung zwischen Systemen für Informations- und für Betriebstechnologie, erklärte eine Sprecherin. Letztere liefen auf speziell abgesicherten Infrastrukturen, die nicht von den betroffenen Microsoft-Diensten abhängig seien.
Im Frankfurter Finanzdistrikt war wie vielerorts die interne Kommunikation gestört. Bankfunktionen seien nicht betroffen und liefen alle ohne Störungen, erklärte ein Sprecher der Commerzbank. Bei der Deutschen Börse hieß es, der Wertpapierhandel laufe wie gewohnt.
Bundesregierung sieht Wirtschaft betroffen
Nach Angaben der Bundesregierung hatte die stundenlange Störung keine größeren Auswirkungen auf die Verwaltung. „Aus der Bundesverwaltung liegen uns keine Meldungen über größere Ausfälle vor“, sagte ein Sprecher des Digitalministeriums in Berlin. Man gehe jedoch von einer großen Betroffenheit in der deutschen Wirtschaft aus. Beim Bundesamt für Sicherheit in der Informationstechnik (BSI) hieß es, von vielen Unternehmen seien Meldungen zum Ausfall bei der Kommunikation eingegangen. Es gebe aber keine Hinweise auf einen Cyberangriff.
Ein Sprecher des Innenministeriums sagte, es gebe bisher keine Kenntnisse darüber, dass das Ministerium oder anhängige Behörden betroffen seien. Der Sprecher des Digitalministeriums erklärte, dass der Bundesclient als Standard-IT-Arbeitsplatz in der Bundesverwaltung stabil laufe. Dieser nutze Microsoft nicht in der Cloud, sondern werde auf eigener Infrastruktur betrieben. Jedoch nutzten noch nicht alle Behörden den Bundesclient, sondern dieser soll bis 2032 Standard in der gesamten Verwaltung werden. Der einheitliche E-Mail-Client in der Bundesverwaltung laufe stabil.
Weiterlesen nach der Anzeige
Internes Microsoft-Problem
Angaben der Microsoft-Ingenieure zufolge wurde auf betroffenen Servern ein Prozess überlastet, der für den Aufbau sicherer Verbindungen zuständig ist – woraufhin die Rechner keine Anfragen mehr verarbeiteten. Zudem machte der Konzern die jüngste Konfigurationsänderung rückgängig, die zeitlich mit dem Beginn der Störung zusammenfiel. Microsoft erklärte, man suche angesichts anhaltender Ungleichgewichte bei der Datenverkehrssteuerung nach Wegen, um die Kapazitäten zu erhöhen.
Ausfälle von Online-Diensten gehören zum Alltag – meist sind sie aber von kurzer Dauer. Manchmal sind die Probleme aber so gravierend, dass es zu stundenlangen Störungen kommt. Microsofts Cloud- und E-Mail-Dienste hatten erst Ende August einen stundenlangen großflächigen Ausfall durchlebt, bei dem sich Nutzer nicht einloggen oder Nachrichten senden und empfangen konnten.
Auswirkungen weltweit
In Australien fiel der Ausfall mitten in die Abschlussprüfungen. Schüler aus Melbourne berichteten dem Sender ABC, sie könnten sich nicht auf ausstehende Sprachprüfungen vorbereiten, weil sie weder auf Materialien noch auf die Website der Prüfungsbehörde zugreifen könnten. Auch Online-Unterricht an Berufsschulen über Microsoft Teams war betroffen. Arzttermine und Untersuchungen mussten verschoben werden. Der Ausfall führte zu Verzögerungen im Flugverkehr. In Sydney musste eine Maschine mit Ziel Papua-Neuguinea am Boden warten, weil der Kapitän seine für den Start erforderlichen Unterlagen nicht per Outlook erhalten hatte.
(nie)
Künstliche Intelligenz
Rust als perfekte Sprache für Agentic AI: Online-Konferenz betterCode() Rust
Am 26. November 2026 findet die sechste Auflage der betterCode() Rust statt. Dieses Jahr legt die Online-Konferenz den Fokus auf agentengetriebene Entwicklung für Rust-Anwendungen.
Weiterlesen nach der Anzeige
Die betterCode() Rust zeigt, welche Architekturen, Tools und Prozesse sich für die agentische Softwareentwicklung mit Rust eignen. Die Vorträge vermitteln Best Practices und Leitlinien, für welche Aufgaben man Agenten sinnvoll einsetzen kann und was man lieber noch selbst macht.
Von Systems Design bis Harness Engineering
Das Programm der Konferenz bietet unter anderem folgende Vorträge:
- Systems Design mit Rust und Agenten
- Sokrates und die Wartbarkeit deiner Rust-Codebasis
- Embedded Sensor mit Agentic Rust entwickeln
- Harness Engineering: Rust als perfekte Sprache für agentische Entwicklung
- Rust in the Age of Agents
Die Konferenztickets sind zum Preis von 299 Euro (alle Preise zzgl. 19 % MwSt.) erhältlich. Teams ab drei Personen erhalten im Online-Ticketshop automatisch einen Gruppenrabatt.
Zusätzlicher Workshop zu Harness Engineering
Am 2. Dezember findet zusätzlich der Workshop „Agent-Ready Rust: Harness Engineering für AI Coding Agents“ statt, der 549 Euro kostet.
Wer über den Verlauf der betterCode()-Konferenz auf dem Laufenden bleiben möchte, kann sich für den Newsletter eintragen.
(rme)
Künstliche Intelligenz
Polarlicht bis Porträt: Licht und Himmel in den Bildern der Woche 46
In dieser Woche steht bei der Bildauswahl aus der c’t-Foto-Galerie der Himmel im Mittelpunkt: Mal dient er als Bühne für die Polarlichter über Norwegen, mal erscheint er als nebliges Grau über den Wolkenkratzern Londons und mal erstrahlt er in goldenem Morgenlicht über den Dächern Berlins. Was alle Aufnahmen verbindet, ist der konsequente Blick auf das Licht und die so geschaffene Atmosphäre. Dabei verändern sich die Stimmungen von Bild zu Bild und entfalten immer eine starke emotionale Wirkung.
Weiterlesen nach der Anzeige
Dazu gesellen sich Motive, die auch die Vielfalt der fotografischen Genres in der Foto-Galerie zeigen: Ein Vogel, präzise aus seinem Umfeld herausgelöst, eine Möwe im Bruchteil einer Sekunde zwischen zwei Tauchgängen, ein gestrandetes Wrack, das durch Langzeitbelichtung und Schwarz-Weiß-Umsetzung zeitlos wirkt – und schließlich ein Porträt, in dem Licht und Schatten zur eigentlichen Aussage werden. Sieben Bilder, sieben Haltungen und eine große Sorgfalt im Blick.
Die Saison ist im vollen Gange von Wolzow1902

Die Saison ist im vollen Gange
(Bild: Wolzow1902)
Wie vertikale Pinselstriche steigen grüne und violette Lichtbänder der Aurora vom Horizont in den tiefblauen Nachthimmel über Norwegen. Die dunkle Silhouette der Hügelkette am unteren Bildrand bildet eine ruhige Grundlinie, vor der sich das Polarlicht umso dramatischer entfaltet. Herbstlich gefärbtes Laub an den Bildrändern rahmt die Szenerie ein und schafft eine spannungsvolle Verbindung zwischen Vordergrund und Himmel. Die Farbskala von tiefem Blau über leuchtendes Grün bis zu zartem Violett verleiht dem Bild eine orchestrale Dynamik.
City of London von M.Schröder

City of London
(Bild: M.Schröder)
Nebel verschluckt die Spitzen dieser Londoner Hochhäuser, er löst die Architektur nach oben hin in ein tonales Grau auf und erzeugt so eine atmosphärische Perspektive. Der zentrale Turm dominiert mit seinem Raster aus Glasflächen das Bild, während ein Baukran an der linken Flanke eine feine vertikale Linie setzt. Rechts schiebt sich ein zweites Gebäude mit markanter Stahlstruktur ins Bild und schafft so eine Staffelung der Bildebenen.
Eisvogel von Lightpix84

Eisvogel
(Bild: Lightpix84)
Ein Eisvogel sitzt auf einem Vorsprung am Wasser und blickt nach oben. Die Aufnahme entstand mit einem Teleobjektiv, das den Hintergrund in ein weiches Bokeh aus warmen Braun- und Grüntönen auflöst. Die geringe Schärfentiefe isoliert den Vogel präzise und lenkt die Aufmerksamkeit auf das leuchtende Türkisblau seines Gefieders, das im Komplementärkontrast zu den orangefarbenen Brustpartien steht. Der Bildaufbau platziert das Tier im unteren Drittel, sodass der weiche, fast malerische Hintergrund viel Raum erhält und eine ruhige Tiefenwirkung entsteht. Die nach oben gerichtete Kopfhaltung des Vogels führt den Blick entlang einer diagonalen Linie durch das Bild und verleiht der Szene eine gewisse Spannung.
Wenn Bäume mal richtig was hermachen von ulwp6

Wenn Bäume mal richtig was hermachen
(Bild: ulwp6)
Aus erhöhter Position blickt die Kamera über eine weite, von Nebelschwaden durchzogene Berliner Landschaft bei Sonnenaufgang. Dutzende Bäume ragen aus dem flachen Dunst hervor und werfen lange, klar gezeichnete Schatten auf den Boden. Im Hintergrund zeichnet sich die Silhouette der Hauptstadt ab: Hochhäuser und der Fernsehturm verschwimmen im goldenen Dunst. Am Horizont schiebt sich die Sonne durch eine Wolkenbank und färbt den Himmel in kräftigen Orange- und Gelbtönen, während darüber bereits kühles Blau durchscheint.
Das Wrack von Asfotografie

Das Wrack
(Bild: Asfotografie)
Gestrandet und verwittert, und doch zieht es den ganzen Blick auf sich. In einer walisischen Bucht liegt dieses alte Boot wie ein Monument der Vergänglichkeit. Es ist umgeben von seidig verwischtem Wasser und ziehenden Wolken. Durch die Langzeitbelichtung wird alles ringsum zur Nebensache, nur das raue Holz des Rumpfes bleibt greifbar und präsent. Die Schwarz-Weiß-Darstellung nimmt der Szene jede Ablenkung und rückt Struktur und Stimmung in den Vordergrund. Ein Bild, das man lange betrachtet – und das dabei immer ruhiger wird.
… und in den Angriff übergehen von Zika

… und in den Angriff übergehen
(Bild: Zika)
Rote Füße, nasses Gefieder und der Blick steil nach unten – diese Lachmöwe, die über dem Wasser kreist, zögert nicht. Gerade ist sie aus dem Wasser aufgestiegen und verharrt für einen Wimpernschlag in der Luft, die Flügel weit aufgespannt. Die feinen Spritzer unter ihr markieren den letzten Tauchgang, während der gesenkte Kopf bereits den nächsten ankündigt. Der ruhige, entsättigte Hintergrund isoliert den Vogel und verleiht dieser Vogelstudie eine fast grafische Klarheit.
Weiterlesen nach der Anzeige
Bernadette von Thomas Ruppel

Bernadette
(Bild: Thomas Ruppel)
Licht, das Streifen malt, und ein Blick, der alles einfängt. Die diagonalen Schattenlinien der Jalousie legen sich wie ein grafisches Raster über Haut, Haar und Hintergrund und erzeugen ein spannungsreiches Muster. Die Schwarz-Weiß-Umsetzung dreht den Kontrast auf und verleiht dem Porträt eine fast skulpturale Wirkung. Die voluminösen Locken des Models brechen das strenge Linienspiel auf organische Weise auf, während die lässig an die Schulter gelegte Hand den Blick zurück zum intensiven Ausdruck lenkt. Hier trifft geometrische Strenge auf natürliche Form.
(vat)
-
Apps & Mobile Entwicklungvor 2 Monatentado°: Smartes Wand-Thermostat ersetzt Batterien durch USB‑C‑Akku
-
Apps & Mobile Entwicklungvor 2 MonatenAqara Spatial Multi-Sensor FP400: Matter-Sensor erkennt bis zu 10 Personen mit mmWave‑Radar
-
Apps & Mobile Entwicklungvor 2 MonatenArm CSS for Mobile 2: C2-Ultra macht die CPU zum Orchestrator für KI‑Agenten
-
Künstliche Intelligenzvor 2 MonatenGesperrte Straße von Hormus: Laut Prognose werden CO₂-Emissionen 2026 sinken
-
Künstliche Intelligenzvor 1 MonatVerbrenner-Aus: Merz und Macron wollen CO₂-Ziel für 2035 weiter lockern
-
Künstliche Intelligenzvor 2 Monaten
Plug-in-Hybride emittieren sechsmal mehr CO₂ im Alltag als offiziell angegeben
-
Apps & Mobile Entwicklungvor 3 MonatenDeutsche Lüfter-Ikone: ebm‑papst geht für 5,1 Milliarden Euro in die USA
-
Künstliche Intelligenzvor 2 MonatenDänischer CO₂-Speicher „Greesand“ geht im Meeresgrund in Regelbetrieb
