Ein Schüler von Shing-Tung Yau hat erneut eine bedeutende Errungenschaft erzielt: Der Beweis der verallgemeinerten Poincaré-Vermutung wurde erstmals formal verifiziert.
Gerade eben gibt es wieder große Neuigkeiten in der Mathematikwelt.
Im September hat die KI die erfolgreiche formale Verifizierung der „Poincaré-Vermutung“ bereits die Mathematikwelt erschüttert.
Gerade jetzt hat ein Spitzenakademikerteam unter der Leitung von Ayush Khaitan in Zusammenarbeit mit dem NVIDIA Humanfia-Team die vollständige Lean-Formalisierung der Thurstons Geometrisierungsvermutung erfolgreich abgeschlossen!
Der „Jahrhundertbeweis“ von Hamilton und Perelman umfasst Hunderte von Seiten, und selbst Spitzenwissenschaftler brauchen mehrere Jahre, um ihn vollständig zu verstehen.
Nachdem die bekannte Poincaré-Vermutung im September dieses Jahres bewiesen wurde, wurde dieser Beweis nun mit Unterstützung von KI zu Zeilen von Code umgewandelt.
4,7 Millionen Codezeilen wurden in nur etwa zwei Wochen erstellt.
Dies ist ein weiterer Meilenstein in der Geschichte der Mathematik und ein Zeichen dafür, dass die KI-gestützte hochdimensionale geometrische Analyse in eine „Ära rasanter Entwicklung“ eintritt.
Die KI-gestützte formale Mathematik ist offiziell in die „Niemandszone“ der tiefgründigsten hochdimensionalen geometrischen Analyse der Menschheit eingetreten.
Erstaunlich! Die Poincaré-Vermutung wurde auf die vollständige Geometrisierungsvermutung erweitert
Wenn Ihnen jemand sagt, dass ein Team in zwei Wochen 4,7 Millionen Zeilen fehlerfreien Codes für moderne Mathematik geschrieben hat, werden Sie sicher denken, dass er verrückt ist.
Aber das ist genau das, was gerade passiert ist.
Kürzlich rief Jared Duker Lichtman, Assistenzprofessor für Mathematik an der Stanford-Universität, aus:
Das ist wirklich eine erstaunliche Arbeit.
Der Beweis der Poincaré-Vermutung wurde auf die vollständige Geometrisierungsvermutung erweitert, und alles wurde vollständig in Lean abgeschlossen!
Derjenige, der das Ergebnis veröffentlicht hat, ist Ayush Khaitan, Mathematiker und KI-Forscher aus Princeton. In seinem Tweet stellte er das starke interdisziplinäre Team vor.
Sehen Sie sich diese beeindruckende Teamliste an:
Bennett Chow: Schüler von Shing-Tung Yau, Professor am Mathematischen Institut der Universität Kalifornien in San Diego, absoluter Autorität und führender Experte auf dem Gebiet des Ricci-Flusses.
Ziyang Qin und Yuan Liao: Die absoluten Hauptverantwortlichen für die formale Arbeit des Projekts.
Ayush Khaitan: Wissenschaftler an der Princeton-Universität, der Hauptförderer des Projekts.
NVIDIA Humanfia-Team (Jui-Hui Chung & Ligeng Zhu): Repräsentiert die Spitzenkraft von NVIDIA, dem weltweit größten Riesen für KI-Rechenleistung.
Unter der Zusammenarbeit dieses Superteams entstand das Wunder.
Ayush enthüllte, dass dieser Beweis etwa 4,7 Millionen Codezeilen umfasst.
Auf der Grundlage der vorherigen Arbeit von Chow, Liao und Qin mit etwa 2 Millionen Codezeilen wurden die zusätzlichen 2,7 Millionen Codezeilen in nur etwa zwei Wochen geschrieben!
Derzeit ist dieses große Projekt vollständig auf GitHub als Open-Source veröffentlicht.
https://github.com/qinz1yang/differential-geometry
Dimensionsschlag: Was haben sie genau bewiesen, von der „Poincaré-Vermutung“ bis zur „vollständigen Geometrisierungsvermutung“?
Warum ist der Mathematiker aus Stanford so aufgeregt?
Zuerst müssen wir wissen, wie schwierig die Thurstons Geometrisierungsvermutung eigentlich ist.
Jeder hat schon von der „Poincaré-Vermutung“ gehört.
Sie lautet: Wenn alle geschlossenen Kurven in einem dreidimensionalen Raum zu einem Punkt zusammengezogen werden können, ist dieser Raum dann notwendigerweise äquivalent zu einer dreidimensionalen Sphäre?
Von 2002 bis 2003 trat das russische Mathematikgenie Grigori Perelman auf, bewies die Poincaré-Vermutung mit drei Preprint-Artikeln und lehnte danach eine Millionen-Dollar-Prämie ab, ohne seine Leistung zur Schau zu stellen.
Aber die Poincaré-Vermutung ist eigentlich nur die „Spitze des Eisbergs“ eines großen Plans. Dieser Plan heißt „Thurstons Geometrisierungsvermutung“.
Mit anderen Worten: Die Poincaré-Vermutung lehrt Sie, wie man eine „Kugel“ erkennt, während die Thurstons Geometrisierungsvermutung eine Art „Periodensystem der Elemente“ für das gesamte dreidimensionale Universum erstellt.
Sie besagt: Jede dreidimensionale Mannigfaltigkeit kann schließlich präzise in mehrere Teile zerlegt werden. Noch wichtiger ist, dass jeder Teil zu einer von acht Standardgeometrien gehört!
Damals bewies Perelman genau durch den Beweis der Thurstons Geometrisierungsvermutung nebenbei die Poincaré-Vermutung.
Sein Zauberwerkzeug heißt „Ricci-Fluss und Operationstheorie“.
Das ist so, als würde man mit einem „geometrischen Bügeleisen“ (der Ricci-Fluss-Gleichung) den verzerrten Raum glätten. Wenn man auf nicht glättbare Knoten (Singularitäten) stößt, führt man eine „chirurgische Operation“ durch, um sie abzuschneiden und zu verschließen, bevor man weiter bügelt.
Diese Theorie ist äußerst tiefgründig. Selbst Dutzende der weltweit besten Mathematiker brauchten zwei bis drei Jahre, um Perelmans Beweis vollständig zu verifizieren.
Und heute haben diese großartigen Wissenschaftler und Ingenieure diese Theorie auf dem Höhepunkt der menschlichen Intelligenz vollständig in den Computer eingebaut!
Der vollständige Lean-Beweis der Thurstons Geometrisierungsvermutung bedeutet, dass Maschinen nun in der Lage sind, fortgeschrittene differentielle Geometrie, Topologie und partielle Differentialgleichungen zu verarbeiten.
Maschinen sind offiziell in die „Niemandszone“ der hochdimensionalen Geometrie eingetreten.
Einblick in das GitHub-Code-Repository: Was genau steht in diesen 4,7 Millionen Codezeilen?
Wenn Sie dieses GitHub-Repository namens differential-geometry öffnen, werden Sie von der harten Fachkompetenz stark beeindruckt.
Link: https://github.com/qinz1yang/differential-geometry
Dies ist eine „digitale Mauer der modernen differentiellen Geometrie“, die in Maschinensprache gebaut wurde.
In Lean, diesem interaktiven Theorembeweiser, kennt der Computer kein „offensichtlich ersichtlich“. Er erkennt nur die untersten logischen Axiome. Um die Maschine die Thurstons Geometrisierungsvermutung verstehen zu lassen, musste das Team von Grund auf alle Regeln des Universums im Code definieren.
Aus den technischen Details des Repositorys geht hervor, dass das Team eine große Anzahl fehlender Grundkomponenten in der offiziellen Lean-Mathebibliothek (Mathlib) ergänzt hat.
Sie haben die Riemannsche Geometrie von Grund auf neu aufgebaut.
Im Code sind äußerst komplexe Mannigfaltigkeiten, Tangentialbündel, Tensorfelder und Riemannsche Metriken definiert.
Mit strenger generischer Programmierung hat das Team die Maschine endlich dazu gebracht, zu „verstehen“, was ein gekrümmter Raum ist.
In traditionellen mathematischen Arbeiten ist der Ricci-Fluss nichts weiter als eine partielle Differentialgleichung.
.
Aber im GitHub-Repository muss das Team mit Tausenden von Codezeilen die „zeitabhängige Entwicklung der Metrik“, die „lokale Berechnung des Ricci-Krümmungstensors“ und die äußerst komplexen Randbedingungen für die Existenz von Lösungen partieller Differentialgleichungen präzise definieren.
Der schwierigste Teil in Perelmans Beweis ist zweifellos die „Operationstheorie“.
Wie implementiert man das „Zuschneiden“ und „Zusammenfügen“ eines abstrakten Raums im Code?
Das Team hat komplexe topologische Verbindungs- und geometrische Zerlegungsalgorithmen in das Code-Repository integriert und die geometrische Singularitätsbehandlung in einen logischen Baum umgewandelt, der von Computern schrittweise ausgeführt und überprüft werden kann.
Rasante Entwicklung in zwei Wochen: NVIDIA steigt ein, große Modelle übernehmen die „Codeproduktionslinie“
Das aufregendste sind diese Zahlen: Zwei Wochen, fast 2,7 Millionen neue Codezeilen, insgesamt 4,7 Millionen Zeilen.
In der Softwareentwicklung reicht ein Projekt mit 2,7 Millionen Codezeilen aus, um ein erfahrenes Entwicklungsteam von Dutzenden von Personen ein ganzes Jahr lang kontinuierlich Überstunden machen zu lassen.
In der Lean-Sprache mit extrem hoher logischer Dichte, bei der jede Codezeile eine sehr lange Kompilierungs- und Überprüfungszeit benötigt, ist es absolut unmöglich, dies in zwei Wochen nur durch menschliche Arbeit zu schaffen!
Wie haben sie das geschafft?
Die Antwort liegt auf der Hand: Das NVIDIA Humanfia-Team hat den „Dimensionsschlag“ durch große Modelle und automatisiertes Schließen gebracht.
NVIDIA bietet nicht nur die stärkste Rechenleistung der Welt, sondern erforscht auch, wie KI die modernste Grundlagenforschung direkt unterstützen kann.
Obwohl die offizielle Seite noch nicht alle Details der KI-generierten Inhalte veröffentlicht hat, lässt sich aus dem kurzfristig stark angestiegenen Codevolumen diese „industrialisierte“ Beweispipeline ableiten.
Spitzenmathematiker wie Chow, Liao und Qin sind dafür verantwortlich, die „Taktikkarte“ zu zeichnen und die große Geometrisierungsvermutung in Tausende von Lemmata und Teilzielen zu zerlegen.
Das NVIDIA-Team nutzt LLM und automatisierte Skripte, um basierend auf dem von Menschen bereitgestellten Kontext massenhaft grundlegende Beweiscodes zu generieren und langwierige algebraische Ableitungen sowie die vollständige Prüfung von Randbedingungen zu ergänzen.
Schließlich werden alle Codes an den Lean-Compiler zur strengen „logischen Qualitätskontrolle“ übergeben. Wenn sie nicht bestehen, werden sie zur Neuschreibung zurückgeschickt, bis das grüne Licht aufleuchtet.
Dies ist nicht nur ein wichtiges Ereignis in der Mathematikwelt, sondern auch ein absoluter Höhepunkt in der Evolutionsgeschichte der KI!
Aktuell leiden große Sprachmodelle noch unter „Halluzinationen“ bei komplexen langkettigen logischen Schlüssen. Die ultimative Waffe zur Behebung der logischen Mängel großer Modelle ist genau die formale Mathematik.
Wenn KI in der Lage ist, geschickt Lean-Code zu generieren, um Produkte auf dem Höhepunkt der menschlichen Intelligenz wie die Thurstons Geometrisierungsvermutung zu beweisen, ist sie nur noch einen Schritt davon entfernt, selbst neue Vermutungen aufzustellen und zu beweisen.
Autobahnen für das mathematische Universum bauen – eine neue Ära hat bereits begonnen
Die vollständige Formalisierung der Thurstons Geometrisierungsvermutung ist weit mehr als nur eine schwierige „Codeübersetzung“. Sie hinterlässt der Welt ein wertvolles digitales Vermächtnis.
Durch das differential-geometry-Projekt auf GitHub hat das Team der gesamten Menschheit eine Bibliothek für differentielle Geometrie