OpenAIs nächstes Modell, Astra, hat gerade zehn seit Jahrzehnten offene Matheprobleme gelöst

Am 1. August veröffentlichte OpenAI einen Bericht, wonach sein nächstes Modell, intern Astra genannt, neue Ergebnisse zu zehn verschiedenen offenen Problemen in der Mathematik erzielt hat. (Nein, es sind nicht die Millennium-Probleme, aber sie sind dennoch von erheblicher Bedeutung.)

Bemerkenswert ist: Diese Lösungen sind kein kleiner Schritt nach vorn, sondern echte Auflösungen der Fragen – verifiziert mit Lean. (Lean ist eine Programmiersprache und ein Beweisassistent, der jede Stufe eines mathematischen Arguments in maschinenlesbaren Details nachvollziehbar macht.) 

Das ist viel auf einmal. In diesem Artikel habe ich die Probleme nach Fachgebieten geordnet und auf hoher Ebene zusammengefasst, was passiert ist, was das für die Mathematik als Disziplin bedeuten könnte und was wir ansonsten über Astra ableiten können.

Was sind die zehn Probleme?

Hier sind die jeweiligen Ergebnisse in einfachen Worten – jeweils mit dem Fachgebiet der Mathematik oder Informatik, zu dem sie gehören.

Nicht-sofische Gruppen

Fachgebiet: Gruppentheorie

Astra konstruierte explizit eine Gruppe, die sich – egal wie genau – nicht durch große endliche Strukturen approximieren lässt. Damit wurde eine seit 1999 offene Frage zum Begriff der „sofischen“ Gruppe geschlossen. Die Konstruktion kommt mit einem Beweis, dass keine Folge endlicher Approximationen je funktionieren kann, formalisiert in Lean, sodass die Logik maschinell geprüft werden kann.

Wikipedia wurde bereits aktualisiert:

Kugelpackungen

Fachgebiet: Hochdimensionale Geometrie

Gefragt ist, wie dicht sich identische, nicht überlappende Kugeln stapeln lassen, wenn die Anzahl der Dimensionen wächst. Astra bewies eine strengere obere Schranke für diese Dichte in hohen Dimensionen – die erste Verbesserung genau dieser Schranke seit 1978. Es liefert keine bessere Packungsmethode, sondern verengt den Bereich dessen, wie gut künftige Methoden maximal sein können.

Binäre und sphärische Codes

Fachgebiet: Kodierungstheorie

Fehlerkorrigierende Codes funktionieren, indem gültige Nachrichten weit genug voneinander entfernt platziert werden, sodass kleine Fehler sie nicht ineinander verwandeln können. Astra bewies deutlich strengere (exponentiell verbesserte) Grenzen für die Anzahl solcher Nachrichten bei gegebenem Mindestabstand – mit einem passenden Resultat für Punkte, die auf einer hochdimensionalen Sphäre verteilt sind.

Connes’ Rigiditätsvermutung

Fachgebiet: Operatoralgebren

Alain Connes vermutete, dass sich bestimmte Gruppen stets eindeutig aus einer aus ihnen aufgebauten algebraischen Struktur – einer von-Neumann-Algebra – rekonstruieren lassen. Astra widerlegte das, indem es zwei wirklich unterschiedliche Gruppen konstruierte, die zur gleichen Algebra führen. Damit ist die Rekonstruktion nicht immer eindeutig.

Arithmetische Schaltkreis-Komplexität

Fachgebiet: Komplexitätstheorie

Die „Permanent“-Funktion, eine einzelne Zahl, die aus einem Zahlenraster berechnet wird, ist aufwendig zu bestimmen. Die Komplexitätstheorie fragt nach der minimal möglichen Anzahl arithmetischer Schritte. Astra bewies eine neue, stärkere untere Schranke für dieses Minimum – eine notorisch schwer zu verbessernde Art von Resultat.

Quanten-parallele Wiederholung

Fachgebiet: Quantenkomplexitätstheorie

Die klassische Theorie besagt: Wenn zwei nicht kommunizierende Spieler ein schwieriges Spiel vielfach parallel wiederholen, sinkt die Erfolgschance für Schummeln exponentiell. Astra bewies, dass diese Garantie auch gilt, wenn die Spieler quantenverschränkt sind – und überträgt damit ein grundlegendes klassisches Prinzip in das Quanten-Setting.

Closest Vector Problem

Fachgebiet: Gitterbasierte Kryptografie

Gegeben ist ein sich wiederholendes Gitter von Punkten (ein Lattice) und ein Zielpunkt. Gesucht ist der nächstgelegene Gitterpunkt – ein Problem, das in hohen Dimensionen als sehr schwer gilt und daher als Fundament für manche quantenresistente Verschlüsselung dient. Astra zeigte, dass selbst die Approximation innerhalb eines bestimmten polynomialen Faktors nachweislich hart bleibt – und stärkt damit die darauf aufbauende Kryptografie.

Ehrharts Volumenvermutung

Fachgebiet: Diskrete und konvexe Geometrie

Für eine konvexe Form, deren einziger innerer Gitterpunkt genau im Schwerpunkt liegt, wollten Mathematiker wissen, welches maximale Volumen eine solche Form in gegebener Dimension haben kann. Astra bestimmte dieses Maximalvolumen für jede Dimension und löste die Vermutung in voller Allgemeinheit.

Mehrfarbige Ramsey-Zahlen

Fachgebiet: Ramsey-Theorie / Kombinatorik

Bei genügend vielen Personen und genügend Beziehungs-Kategorien findet man zwangsläufig drei Personen, die alle durch dieselbe Kategorie verbunden sind. Astra zeigte, dass die dafür nötige minimale Gruppengröße schneller wächst als jede feste Exponentialrate, wenn die Zahl der Kategorien steigt – und löste damit Erdős’ Problem 183.

Extremalzahl-Vermutungen

Fachgebiet: Extremale Graphentheorie

Dieses Teilgebiet fragt, wie viele Kanten ein Netzwerk haben kann, ohne bestimmte kleine, verbotene Muster zu enthalten. Astra klärte zwei verwandte Vermutungen (Erdős’ Probleme 146 und 180) und legte damit fest, wie dicht solche Netzwerke werden können, bevor diese Muster unvermeidbar auftreten.

Jedes dieser Probleme war seit mindestens einem Jahrzehnt offen; einige sogar seit dreißig Jahren und länger – darunter Fragen, an denen Turing-Preisträger auf der theoretischen Informatikseite gearbeitet haben.

Moment – ist ein Gegenbeispiel die „einfache“ Art von Beweis?

Wer bin ich, hier etwas Negatives zu sagen – aber ich weiß, dass diese Frage oder Reaktion häufig kommt, gerade von Menschen mit Mathekenntnissen.

Die gängigste Kritik lautet: Mehrere dieser Ergebnisse sind Gegenbeispiele statt neue allgemeine Theorie. Das ist relevant, weil ein Gegenbeispiel eine Ja/Nein-Frage beantwortet, aber für sich allein nicht erklärt, weshalb ein Muster bricht oder gleich eine Familie ähnlicher Objekte zum Weiteruntersuchen liefert. Eine Klassifikation oder eine neue Methode öffnet hingegen mehr Türen.

Ich würde sagen, diese Kritik ist im Allgemeinen berechtigt, taugt aber nicht als pauschale Abwertung des gesamten Bündels. Erstens ist das Resultat zu nicht-sofischen Gruppen keine kleine Anpassung eines Beinahetreffers – es ist die erste Konstruktion ihrer Art nach 27 Jahren, in denen es keinerlei Beispiel gab, und die zugrunde liegende Technik dürfte sich verallgemeinern lassen, um weitere zu finden.

Zweitens sind mehrere der übrigen neun Resultate – darunter die Schranke zur Kugelpackung und die Härte des CVP – gar keine Gegenbeispiele, sondern direkte Verbesserungen bestehender Schranken. 

Was noch offen ist

Einige Punkte sollte man verfolgen, während das Feld die Ergebnisse in den kommenden Tagen, Wochen und Monaten auseinandernimmt:

\n
• Noch kein Peer Review. Die Beweise sind in Lean verifiziert und wurden informell von Mathematikerinnen und Mathematikern mit Vordrucken begutachtet, aber keiner ist bislang durch ein formales, begutachtetes Journalverfahren gegangen. 
\n
• Autorschaft wird noch verhandelt. OpenAI erklärt, für Manuskripte und Lean-Formalierungen verantwortlich zu sein, während die mathematischen Argumente selbst dem Modell zugeschrieben werden. Eine unabhängige Replikation des Prozesses (im Gegensatz zur Verifikation der Beweise) ist derzeit schwer umzusetzen.
\n

Was das für die Mathematik bedeutet

Die unmittelbarste Verschiebung betrifft die Frage, womit Mathematikerinnen und Mathematiker tatsächlich ihre Zeit verbringen. Wenn sich ein klar formuliertes offenes Problem einem Modell übergeben und in Lean prüfen lässt, verlagert sich der Engpass von „Kann das jemand lösen?“ zu „Haben wir die richtige Frage gestellt und korrekt formalisiert?“. Das Stellen guter Fragen und das Erkennen, welches Problem sich lohnt, ist eine echte, erfahrungsbasierte Kompetenz.

Auch Förder- und Glaubwürdigkeitsfragen kochen hoch. Forschungsförderung, Tenure-Verfahren und Preise beruhten historisch auf Knappheit: Diese Probleme waren so schwer, dass ihre Lösung etwas über die Lösenden aussagte. Wenn KI-gestützte Ergebnisse zur Routine werden, braucht das Feld neue Wege, um zu signalisieren, was wirklich schwer ist und was nun mit ein paar tausend Dollar Inferenz erreichbar ist. Klar, die breite Öffentlichkeit versteht diese Probleme nicht im Detail. Die Menschen mit echter Ausbildung tun es – das ändert sich nicht. Mathematisches Wissen ist damit wertvoller denn je. 

Wie die Reaktionen ausfallen

Die Reaktionen in sozialen Medien spalteten sich weniger an der Frage, ob die Beweise stimmen, sondern eher daran, was sie belegen.

Manche sehen das Tempo als eigentliche Story: zehn seit Jahrzehnten offene Probleme auf einen Schlag, über nicht zusammenhängende Felder hinweg – schneller, als Fachleute sie prüfen können. Eine Frage für die Zukunft: „Werden wir mit dem Prüfen noch hinterherkommen?“

Andere wenden ein, dass das weniger über KI im Allgemeinen aussagt, als es scheint. Mathematik ist ein seltenes Gebiet, in dem sich die Arbeit eines Modells automatisch und vollständig prüfen lässt. Die meisten realen Probleme bieten keinen solchen eingebauten, automatischen Lösungsschlüssel. In dieser Sicht ist die Leistung real, sagt aber eher, dass Mathematik für KI ungewöhnlich gut geeignet ist.

Ein dritter Strang der Kommentare: Ein korrekter Beweis, den noch niemand vollständig geprüft oder inhaltlich durchdrungen hat, ist noch nicht wirklich verstanden – nur verifiziert. Einen Satz entdecken und seine Bedeutung begreifen, sind in dieser Sicht zwei verschiedene Aufgaben.

Abschließende Gedanken

Mathematikerinnen und Mathematiker sagen, das Resultat zu nicht-sofischen Gruppen wirkt wie „in echt“: eine echte, seit Jahrzehnten offene Frage der Gruppentheorie, gelöst durch eine explizite Konstruktion, die in der Fachcommunity ernst genommen wird. Die übrigen neun Ergebnisse stehen zusammen für einen breiten, technisch anspruchsvollen Schub quer durch die reine Mathematik.

Was noch aussteht, ist der langsamere Teil: Peer Review, Replikation des Suchprozesses und dass das Feld tatsächlich auf diesen Ergebnissen aufbaut. Das dauert länger als einen Blogpost – und erst das wird zeigen, wie groß das wirklich war. Wir halten dich auf dem Laufenden.