Chinesisches KI-Modell beweist erstmals 3D-Ghys-Vermutung

Das Shanghai AI Laboratory hat gemeinsam mit Forscher:innen der Guangzhou Bay University unter Leitung von Professor Xu Disheng die dreidimensionale Ghys-Vermutung gelöst. Damit wurde erstmals ein seit über dreißig Jahren offenes Weltproblem der Mathematik mit einem chinesischen Large Language Model bewältigt. Die Arbeit basiert auf dem Multimodal-Modell ShuSheng-S2 und etabliert einen neuen, reproduzierbaren Forschungsmodus in der KI-gestützten Grundlagenwissenschaft. Die Modellentwicklung folgte einer gezielt ausgelegten Allgemein-zu-Spezial-Strategie. Nach starken Leistungen im nationalen chinesischen Mathematikwettbewerb 2025 wurden die Trainingsdaten und Algorithmen auf forschungsnahe Mathematik zugeschnitten. Durch asynchrones Langzeit-Räsonanz-Verstärkungslernen und eine hochspezifische Nachtrainierung mit Peer-Review-Daten überwanden die Entwickler fundamentale technische Hürden wie exponentielle Fehlerakkumulation und konsistente Selbstkorrektur. Das finale System zählt international zu den leistungsstärksten Open-Source-Modellen für langkettige Deduktion und erreicht in mehreren Benchmarks ein Niveau, das geschlossene kommerzielle Modelle übertrifft. Der eigentliche Durchbruch bei der Ghys-Vermutung entstand durch iterative menschlich-künstliche Zusammenarbeit. Die 1995 formulierte Vermutung aus dem Bereich komplexer Dynamiksysteme behandelt die mathematische Starrheit holomorpher Anosov-Systeme. ShuSheng-S2 produzierte initiale 400 Seiten abgeleiteter Schlussfolgerungen und generierte dabei Dutzende neuartige Beweisstrategien. Professor Xu und sein Team, ergänzt durch Doktorand Zhang Jiesong vom Kungliga Tekniska Högskolan, filterten die vielversprechendsten Ansatzpunkte, kalibrierten die KI-Richtung und ließen das System über sieben Iterationsrunden weiterführen. Das zugrundeliegende Problemgraphen wuchs dabei von 15 auf 389 Knoten an, wobei über tausend Seiten streng logisch verknüpfter Texte entstanden. Die Validierung erfolgte durch ein Team der Peking-Universität unter Professor Dong Bin und Akademiker Liu Ruochuan. Mithilfe ihres SHEAF-Frameworks wurden alle vier Hauptsätze des Papiers vollständig im Beweisassistenten Lean formal verifiziert. Innerhalb von fünf Tagen prüften bis zu hundert parallele KI-Agenten rund fünfhundertfünfzigtausend Zeilen Lean-Code. Der Prozess schloss nicht nur semantische Lücken, sondern baute auch die zuvor fehlende formale Infrastruktur für dynamische Systeme auf. Unabhängige Gutachter betonten die historische und theoretische Bedeutung der Lösung. Die auf arXiv veröffentlichten Ergebnisse demonstrieren einen Paradigmenwechsel: Statt isolierter menschlicher Intuition entsteht ein geschlossener Kreislauf aus systematischer KI-Erkundung, Expertenfilterung und automatischer Reifung. Shanghai AI Laboratory plant, die erarbeiteten Bausteine in die wissenschaftliche Entdeckungsplattform Shusheng-Duan Yan zu integrieren, um die Methode auf weitere formale Wissenschaften zu übertragen. Parallel sucht das Labor kontinuierlich nach internationalen Gastwissenschaftlern, um an der Schnittstelle von menschlicher Expertise und maschineller Deduktion neue Grenzen der mathematischen Informatik zu verschieben.