Anthropic hat am 5. September einen Meilenstein für KI in der Mathematik gemeldet: Das Sprachmodell Claude erzeugte den ersten vollständig maschinell geprüften Beweis der Fermatschen Vermutung in der Beweissprache Lean – in nur elf Tagen und weitgehend autonom.
Was Claude geleistet hat
In elf Tagen Rechenzeit schrieb Claude nach Angaben von Anthropic rund 13 Millionen Zeilen Lean-Code und bewies dabei etwa 29.500 Zwischentheoreme, die in den finalen Beweis einflossen. Das Ergebnis ist damit mehr als fünfmal so umfangreich wie die etablierte Mathematik-Bibliothek Mathlib. Verbraucht wurden rund sechs Milliarden Ausgabe-Tokens eines internen Forschungsmodells, verteilt auf mehrere parallel arbeitende Agenten.
- Dauer: 11 Tage, weitgehend autonom
- Umfang: rund 13 Millionen Zeilen Lean-Code
- Zwischentheoreme: etwa 29.500 im finalen Beweis
Wie die Agenten zusammenarbeiteten
Mehrere Claude-Instanzen teilten die Arbeit über die Plattform Prove2Me auf, die der Forscher Tianyi Peng mit Kollegen an der Columbia University entwickelt hat. Erste Versuche scheiterten, weil die Agenten den Überblick über den Projektstand verloren und die Zusammenarbeit abbrach. Erst Prove2Me – das die Theoreme in einem gerichteten Graphen verwaltet und die Lean-Kompilierung beschleunigt – ermöglichte die koordinierte Formalisierung.
Einordnung
Der Mathematiker Kevin Buzzard vom Imperial College London prüfte den Beweis und sprach von einer außergewöhnlichen Autoformalisierungs-Leistung, die die Fermatsche Vermutung ohne weitere Annahmen als die Axiome der Mathematik belege. Anthropic räumt zugleich ein, dass die generierte Fassung wahrscheinlich viel länger als nötig ausfalle. Der Durchbruch zeigt dennoch, wie KI-Agenten formale Mathematik künftig automatisieren könnten.
Quellen: Anthropic Research · The Next Web
