Chinesisches KI-Modell hilft, dreidimensionale Ghys-Vermutung zu beweisen; Lean prüft die Mathematik

Mathematikproblem aus dem Jahr 1995 erreicht einen neuen Meilenstein

Eine 1995 aufgestellte mathematische Vermutung ist nun für den Fall der komplexen Dimension drei bewiesen worden. Möglich wurde dies durch die Zusammenarbeit von Mathematikern mit dem Modell Intern-S2 des Shanghai AI Laboratory. Anschließend übertrug ein Team der Peking-Universität die vier Hauptsätze der Arbeit in Beweise, die mit Lean geprüft wurden, einem Computersystem zur Verifikation mathematischer Schlussfolgerungen.

Das Shanghai AI Laboratory gab den Erfolg am 15. Oktober 2026 bekannt. Es würdigte ein Team unter der Leitung von Disheng Xu, Professor an der Great Bay University und Gastwissenschaftler am Labor. Die Forschungsarbeit „Codimension-one holomorphic Anosov diffeomorphisms“ nennt Jiesong Zhang vom schwedischen KTH Royal Institute of Technology als alleinigen Autor.

Das Ergebnis löst den Kodimension-eins-Fall der Vermutung des französischen Mathematikers Etienne Ghys, einschließlich des Falls der komplexen Dimension drei. Es geht um einen bemerkenswerten Zusammenhang zwischen Bewegung und Form: Muss ein Raum, in dem eine bestimmte Art chaotischer Bewegung möglich ist, selbst eine hochgeordnete mathematische Struktur haben?

Intern-S2 half, durch wiederholten Austausch mit den Forschern Ideen und Argumente zu entwickeln. In seiner Erklärung zur Verwendung von KI gibt Zhang an, die gesamte Mathematik eigenständig überprüft zu haben. Die Zusammenarbeit verband maschinelle Exploration, menschliches Urteilsvermögen und ein separates Verfahren zur formalen Verifikation.

Das Labor bezeichnet den Erfolg als ersten Einsatz eines chinesischen KI-Modells zur Unterstützung bei der Lösung eines mathematischen Problems dieser Bedeutung. Das konkrete Ergebnis ist ein Klassifikationssatz, der von einem öffentlich zugänglichen Preprint und veröffentlichter Formalisierungssoftware begleitet wird.

Was der Beweis über Bewegung und Form aussagt

Ghys' Vermutung gehört zur komplexen Dynamik. Sie untersucht, wie sich mathematische Systeme verändern, wenn ihre Koordinaten den Regeln komplexer Zahlen folgen. Eine komplexe Zahl hat zwei reelle Komponenten, daher entsprechen drei komplexe Dimensionen lokal sechs reellen Dimensionen. Der Rahmen ist abstrakter als ein gewöhnliches Objekt, das sich durch einen Raum bewegt.

Ein Anosov-System weist eine präzise Kombination aus Dehnung und Stauchung auf. Bei wiederholter Bewegung ziehen sich manche Richtungen zusammen, während andere sich ausdehnen. Benachbarte Ausgangspunkte können sich schnell voneinander entfernen. So entsteht chaotisches Verhalten, obwohl die Regel für jeden einzelnen Schritt exakt festgelegt ist.

Anschaulich lässt sich das mit einem wiederholten Vorgang vergleichen, bei dem eine Form gedehnt und gefaltet wird. Das hier untersuchte mathematische System ist jedoch deutlich restriktiver: Seine Dehnung und Kontraktion müssen einheitlichen Bedingungen genügen, und seine Bewegung muss die durch komplexe Koordinaten vorgegebene Struktur erhalten.

Ghys vermutete, dass solche Systeme auf kompakten komplexen Mannigfaltigkeiten eine standardisierte algebraische Beschreibung haben sollten. Eine Mannigfaltigkeit ist ein Raum, der in einer kleinen Umgebung einfach aussieht, auch wenn seine Gesamtform kompliziert ist. Kompaktheit ist in diesem Zusammenhang eine mathematische Bedingung, die verhindert, dass sich der Raum unbegrenzt erstreckt.

Zhangs Satz besagt, dass jede holomorphe Anosov-Diffeomorphie der Kodimension eins auf einer kompakten, zusammenhängenden komplexen Mannigfaltigkeit biholomorph konjugiert zu einem hyperbolischen Automorphismus eines komplexen Torus ist. Einfacher gesagt: Eine umkehrbare Koordinatentransformation, die die komplexe Struktur respektiert, überführt die Bewegung in eine standardisierte algebraische Transformation auf einem sehr regelmäßigen Raum.

Ein komplexer Torus lässt sich konstruieren, indem man Punkte im komplexen Raum identifiziert, die sich um Elemente eines periodischen Gitters unterscheiden. Die zentrale Leistung besteht darin, dass die komplizierte Dynamik diese geordnete geometrische Beschreibung erzwingt.

Warum der genaue Geltungsbereich wichtig ist

Die Arbeit behandelt den Fall der Kodimension eins. Bei diesen Systemen bedeutet das, dass einer der kontrahierenden oder expandierenden Teile komplexe Dimension eins hat. Der Satz gilt allgemein für diese eingeschränkte Familie und löst die Vermutung in der komplexen Dimension drei.

Ghys' umfassendere Vermutung betrifft holomorphe Anosov-Systeme auf einem breiteren Spektrum komplexer Mannigfaltigkeiten und beschreibt sie mithilfe standardisierter algebraischer Modelle auf sogenannten komplexen Infranilmannigfaltigkeiten. Zhangs Ergebnis liefert für den untersuchten Fall eine besonders strenge Antwort: einen komplexen Torus und einen hyperbolischen Automorphismus.

Für Mathematiker, die an diesem Fall arbeiten, verlagert der Satz die Fragestellung: Statt einen unbekannten Raum und eine unbekannte Bewegung zu bestimmen, können sie ein standardisiertes Modell untersuchen. Eine Koordinatentransformation verbindet das ursprüngliche System mit diesem Modell und bewahrt dabei die komplexe Geometrie.

Xu hatte sich jahrelang mit dem Problem beschäftigt. Gemeinsam mit seinem früheren Betreuer, dem Fields-Medaillen-Träger Artur Avila, untersuchte er zuvor den Fall in Dimension drei. Xu und Zhang erzielten später partielle, verwandte Ergebnisse, die im Journal of the European Mathematical Society veröffentlicht wurden. Die neue Arbeit baut auf dieser langjährigen Beschäftigung mit derselben mathematischen Frage auf.

Von einer Olympiadeaufgabe zu einer Forschungspartnerschaft

Intern-S2s Einsatz knüpfte an ein früheres Ergebnis von Intern-S1 bei der Chinesischen Mathematik-Olympiade 2025 an. Das für Mathematikwettbewerbe an weiterführenden Schulen zuständige Komitee der Chinesischen Mathematischen Gesellschaft führte in jenem Jahr einen KI-Test ein. Drei chinesische Modelle sollten Aufgaben innerhalb derselben Zeitvorgabe wie die menschlichen Teilnehmer lösen.

Intern-S1 erreichte nach denselben Bewertungsmaßstäben 102 Punkte und belegte damit unter den drei teilnehmenden Modellen den ersten Platz. Die Goldmedaillenschwelle lag bei 78 Punkten. Das Modell lag somit 24 Punkte darüber, also rund 31 Prozent.

Xu sah Potenzial darin, die Modellfamilie in der mathematischen Forschung einzusetzen, während das Shanghai AI Laboratory von Wettbewerbsaufgaben zu ungelösten Fragen übergehen wollte. Die Zusammenarbeit begann Anfang 2026. Dazu gehörte die Entwicklung eines Softwaresystems, eines sogenannten Harness, das die Arbeit des Modells und den Austausch mit den Forschern koordinieren sollte.

Die wichtigsten Etappen waren:

• 1995: Etienne Ghys stellte die Vermutung auf.
• 2025: Intern-S1 erreichte im KI-Test der Chinesischen Mathematik-Olympiade 102 Punkte.
• Anfang 2026: Xu und das Shanghai AI Laboratory begannen mit der Zusammenarbeit zum Modelltraining.
• März 2026: Xu wurde Gastwissenschaftler am Labor.
• August 2026: Eine intern entwickelte Version von Intern-S2 und das zugehörige System erreichten den Stand, der für intensive mathematische Exploration genutzt wurde.
• 29. September: Zhangs Arbeit wurde auf arXiv veröffentlicht, am 13. Oktober folgte eine überarbeitete Fassung.
• 15. Oktober 2026: Der Erfolg wurde öffentlich bekannt gegeben.

Wie die Mathematiker die KI anleiteten

Intern-S2s erste Untersuchung des Problems führte zu einem rund 400 Seiten langen Herleitungsbericht. Xu lud Zhang, seinen früheren Studenten und Postdoktoranden am KTH, ein, sich als Gastwissenschaftler an der Arbeit zu beteiligen. Zhang hatte die Ghys-Vermutung schon während seiner Promotion verfolgt.

Xu und Zhang prüften die Vorschläge des Modells, identifizierten vielversprechende Ansätze und gaben Rückmeldungen, um die weitere Exploration zu lenken. Die Maschine verfolgte verschiedene Argumentationswege und generierte Begründungen. Die Mathematiker entschieden, welche Richtungen eine weitere Untersuchung verdienten, und halfen dabei, den abschließenden Beweis zusammenzustellen.

Das Labor beschreibt sieben Durchläufe mit fortgesetzter Argumentation. Im Verlauf wuchs der Problemgraph des Modells von 15 auf 389 Knoten. Die gesammelten Ausgaben umfassten rund tausend Seiten und Dutzende vorgeschlagene Ansätze.

Ein Problemgraph bildet kleinere mathematische Aufgaben und ihre Verbindungen ab. Ein Knoten kann etwa eine Zwischenaussage darstellen, ein anderer ein Ergebnis, das zu ihrem Beweis benötigt wird. Der gemeldete Zuwachs zeigt, wie umfassend das System das Problem aufteilte und untersuchte.

Zhangs Erklärung zur Verwendung von KI macht deutlich, wer für die fertige Mathematik verantwortlich ist: Eine interne Version von Intern-S2 half in mehreren Dialogrunden dabei, Ideen und Argumente zu entwickeln; Zhang überprüfte die Mathematik eigenständig. In seiner Arbeit dankt er Xu außerdem für die fortlaufenden Diskussionen.

Welchen Beitrag die unterstützende Software leistete

Das Shanghai AI Laboratory kombinierte das Modell mit einer Software, die lange Argumentationsketten und wiederholte Rückmeldungen von Menschen verwalten sollte. Das System konnte eine schwierige Frage in kleinere Aufgaben aufteilen, mehrere Ansätze untersuchen und Ergebnisse zur Bewertung an die Forscher zurückgeben.

Der Trainingsansatz verband umfassendes wissenschaftliches Wissen mit Material zur mathematischen Forschung. Dazu gehörten schwierige Aufgaben aus mathematischen Facharbeiten und Methoden zur Überprüfung vorgeschlagener Lösungen. Das Labor beschreibt außerdem den Einsatz von Reinforcement Learning mit verifizierbaren Belohnungen. Das bedeutet, dass erfolgreiche, überprüfbare Argumentationen als Trainingssignal dienen konnten.

Anschließend nutzten die Forscher Erkenntnisse aus dem unterstützenden System, um das Modell selbst zu verbessern. Ziel in der Praxis war es, den Fortschritt über eine lange Untersuchung hinweg aufrechtzuerhalten, Zwischenergebnisse nachzuverfolgen und Fehler zu korrigieren, während neue Argumente entwickelt wurden.

Das Labor verwies zudem auf Ergebnisse bei IMO-Proof und AdvancedMathBench, zwei Tests mit Schwerpunkt auf mathematischem Schlussfolgern. Für das Ghys-Projekt sind die detailliertesten Belege für die Funktionsweise des Systems die Abfolge umfangreicher Herleitungen, Rückmeldungen von Experten, eine fertige Forschungsarbeit und die anschließende formale Verifikation.

Wie das Team der Peking-Universität den Beweis prüfte

Das von Bin Dong und Ruochuan Liu geleitete Team der Peking-Universität nutzte sein SHEAF-Framework, um alle vier Hauptsätze in Zhangs Arbeit zu formalisieren. Die Arbeit umfasste auch Ergebnisse von Ghys, auf denen die Argumente beruhen.

Bei der Formalisierung werden mathematische Definitionen, Annahmen und Schlussfolgerungen in eine Sprache übertragen, die ein Computer prüfen kann. In einer herkömmlichen Forschungsarbeit kann man darauf vertrauen, dass fachkundige Leser vertraute Schritte ergänzen. Lean verlangt, dass diese Schritte durch präzise Aussagen und zulässige logische Operationen ausgedrückt werden.

Die Teammitglieder Jiedong Jiang und Bin Wu zufolge dauerte die Arbeit etwa fünf Tage. Dabei waren bis zu 100 KI-Agenten parallel im Einsatz. Das Ergebnis umfasste rund 550.000 Zeilen Lean-Code. Experten prüften außerdem, ob die formalen Aussagen der mathematischen Bedeutung der Hauptsätze in der Arbeit entsprachen.

SHEAF organisierte die Aufgabe als gerichteten Graphen aus Definitionen, Aussagen und Abhängigkeiten. So konnten verschiedene Agenten an miteinander verbundenen Teilen arbeiten, während das Team nachverfolgte, welche Aussagen bereits bewiesen waren und bei welchen noch Arbeit nötig war.

Die Formalisierung erforderte mehr als die Übertragung der abschließenden Argumente. Einige unterstützende Ergebnisse aus der Dynamik fehlten in bestehenden Bibliotheken für formal verifizierte Mathematik. Das Team musste diese Grundlagen selbst ergänzen oder Wege finden, bereits verfügbare Ergebnisse zu nutzen, und anschließend alle Teile zu einer lückenlosen Beweiskette verbinden.

Die Arbeit ist als arXiv-Preprint verfügbar, der Formalisierungscode wurde auf GitHub veröffentlicht. In der Ankündigung wurden weder eine Veröffentlichung in einer Fachzeitschrift noch eine Entscheidung über ein Peer-Review-Verfahren genannt.

Warum die beiden Etappen zusammengehören

Intern-S2 und SHEAF erfüllten unterschiedliche Aufgaben. Das erste System unterstützte die Suche nach mathematischen Ideen und Argumenten. Das zweite half dabei, formale Beweise zu erstellen, die Lean prüfen konnte. Die Mathematiker lenkten die Exploration, überprüften die daraus entstandene Mathematik und beurteilten, ob die formalen Aussagen den gemeinten Sätzen entsprachen.

Der Umfang der Arbeit macht diese Aufgabenteilung konkret: Aus rund tausend Seiten explorativer Ergebnisse entstand eine Forschungsarbeit; bei der Verifikation kamen anschließend etwa 550.000 Zeilen formalen Codes zusammen. Jede Etappe überführte die Arbeit in eine andere Form, passend zu einer jeweils anderen Aufgabe.

Für künftige Forscher bietet die öffentlich zugängliche Arbeit das mathematische Argument, während der veröffentlichte Code die Struktur des formalen Beweises dokumentiert. Die bei der Formalisierung ergänzten Definitionen und Ergebnisse können außerdem als Ausgangspunkt für weitere Arbeiten auf diesem Gebiet dienen.

Der nächste Schritt ist ein wiederverwendbares Verifikationsmodul

Das Shanghai AI Laboratory plant, den Arbeitsablauf als mathematisches Verifikationsmodul für seine Plattform Intern Duanyan zur wissenschaftlichen Entdeckung aufzubereiten. Ziel ist es, die Kombination aus Modell-Exploration, Rückmeldungen von Experten und formaler Prüfung für spätere Projekte wiederverwendbar zu machen.

Das Labor will die im Projekt entwickelten Schlussfolgerungsfähigkeiten außerdem auf andere Fachgebiete mit verwandten mathematischen Strukturen anwenden. Vorgesehen ist ein Kreislauf: ein Forschungsproblem lösen, nützliche Methoden in wiederverwendbare Software überführen und sie bei einer weiteren Untersuchung einsetzen.

Für Xu führt das Ergebnis ein langjähriges Forschungsinteresse fort, getragen von der Zusammenarbeit zwischen der Great Bay University, dem Shanghai AI Laboratory, dem KTH und der Peking-Universität. Für die breitere mathematische Gemeinschaft bietet es sowohl ein neues Klassifikationsergebnis als auch ein detailliertes Beispiel dafür, wie KI unter menschlicher Anleitung an der Forschung mitwirken kann.

Wichtige Punkte

• Der neue Beweis löst den Kodimension-eins-Fall der Ghys-Vermutung, einschließlich der komplexen Dimension drei.
• Jiesong Zhang ist alleiniger Autor der Forschungsarbeit und gibt an, die gesamte Mathematik eigenständig überprüft zu haben.
• Disheng Xu und Zhang lenkten Intern-S2 durch wiederholte Exploration und Rückmeldungen.
• Der Problemgraph des Modells wuchs von 15 auf 389 Knoten; die Herleitungen umfassten rund tausend Seiten.
• Das SHEAF-Framework der Peking-Universität half dabei, vier Hauptsätze und unterstützende Ergebnisse in Lean zu formalisieren.
• Die Verifikation dauerte laut Angaben etwa fünf Tage und erzeugte rund 550.000 Zeilen Code.
• Das Labor plant, den Arbeitsablauf in ein wiederverwendbares mathematisches Verifikationsmodul zu überführen.