AI Agent hat die Formalisierung des ersten Fields-Preises-Ereignisses des Jahrhunderts abgeschlossen, unabhängig in einer Woche erledigt, und 200.000 Codezeilen wurden veröffentlicht.

In nur 5 Tagen hat KI die formale Beweis eines Mathematik-Ergebnisses auf Fields-Medaille-Niveau abgeschlossen, das normalerweise 6 Monate dauern würde.

Sobald dieses neueste Ergebnis veröffentlicht wurde, löste es sofort eine Diskussion auf X aus. Einige Mathematiker nennen es sogar das "ImageNet-Moment im Bereich der automatischen Formalisierung".

Die KI ist die von der Firma Math entwickelte KI namens Gauss. Konkret hat sie die formale Verifikation des Ergebnisses durchgeführt, für das Maryna Viazovska 2022 die Fields-Medaille, den höchsten Mathematikpreis, erhalten hat: dem Theorem über das optimale Kugelpackproblem in 8 und 24 Dimensionen.

Dies ist das erste Mal seit Beginn dieses Jahrhunderts, dass ein Fields-Medaille-Ergebnis vollständig formalisiert wurde.

Mit 200.000 Zeilen Lean-Code für ein einzelnes Projekt hat diese neueste Arbeit von "Silizium-Gauss" das größte Einzelsystem-Projekt in der Geschichte der Lean-Formalisierung geschaffen.

Ein weiterer Punkt, der die Aufmerksamkeit auf sich zog, ist, dass "Silizium-Gauss" während des Inferenz- und Verifikationsprozesses selbständig Fehler in der ursprünglichen Dissertation erkannt und korrigiert hat.

Erste Formalisierung eines Fields-Medaille-Ergebnisses in diesem Jahrhundert

2022 erhielt Maryna Viazovska die Fields-Medaille, weil sie bewies, dass das E8-Gitter in 8 Dimensionen die dichteste Packung gleicher Kugeln bietet, und für ihre weiteren Beiträge zum relativen Extremwertproblem und zur Fourier-Analyse.

Das hier erwähnte Kugelpackproblem war das, auf das sich "Silizium-Gauss" konzentrierte.

Einfach ausgedrückt, geht es darum zu beweisen, wie dicht gleiche Kugeln in einem n-dimensionalen Raum maximal gepackt werden können.

In der eindimensionalen Situation ist dieses Problem nicht kompliziert, und in der zweidimensionalen Situation gibt es bereits einen Beweis. Aber wenn n auf 3 steigt, also in der dreidimensionalen Situation, obwohl Johannes Kepler 1611 die entsprechende Vermutung aufstellte, gelang es dem Mathematiker Thomas Hales erst 1998, mit Computerunterstützung den Beweis zu führen; und die formale Verifikation der dreidimensionalen Situation dauerte noch weitere zehn Jahre.

In höheren Dimensionen wird das Problem noch komplexer und schwerer zu lösen. Bis Maryna Viazovska den Zusammenhang zwischen diesem Problem und der Theorie der Modulformen fand -

Sie verwendete eine innovative Methode, die Fourier-Analyse und Modulformen kombiniert, um eine optimierte Hilfsfunktion zu konstruieren, um die Optimalität des E8-Gitters in 8 Dimensionen streng zu verifizieren.

Basierend auf derselben Methode bewies sie zusammen mit ihren Mitarbeitern weiter, dass das Leech-Gitter die dichteste Kugelpackung in 24 Dimensionen bietet.

△Generiert durch KI

2024 begann Maryna Viazovska zusammen mit ihren Mitarbeitern, ein Projekt zur Formalisierung dieses Ergebnisses zu initiieren.

Formalisierung bedeutet, dass mathematische Beweise streng in einer formalen Sprache ausgedrückt werden, die den Regeln der formalen Logik entspricht. Dieser Prozess kann von einem Computer verifiziert werden, um sicherzustellen, dass jeder Schritt des Beweises vollständig den logischen Regeln entspricht. Das Hauptziel ist es, die Strenge, Zuverlässigkeit und Transparenz der Mathematik zu verbessern.

Im November 2025 begann "Silizium-Gauss" an diesem Projekt teilzunehmen. Nachdem es einige Probleme bezüglich Modulformen, radialer Schwartz-Funktionen und der Grundlagen des Kugelpackproblems bewiesen hatte, war das Ziel dieser KI, die gesamte verbleibende Arbeit des Projekts automatisch abzuschließen.

Also entwickelte sich die Sache über die Vorstellung der Menschen hinaus:

In den ersten zwei Jahren schrieb ein Team menschlicher Experten insgesamt etwa 20.000 Zeilen Lean-Code. Gauss hingegen hat in nur 5 Tagen etwa 50.000 Zeilen Code hinzugefügt und die Verifikation der 8-dimensionalen Situation dieses Problems abgeschlossen, ohne zusätzliche Hilfsrahmen zu verwenden.

Das Team schätzte ursprünglich, dass es mit den vorhandenen Werkzeugen noch 6 Monate dauern würde, um dieses Projekt abzuschließen.

Noch eine Woche später, nachdem Gauss die ursprüngliche Dissertation von Viazovska und über 20 zusätzliche Referenzen studiert hatte, hat es 450.000 Zeilen Code generiert und auch die formale Beweis der 24-dimensionalen Situation abgeschlossen.

Das Team hinter "Silizium-Gauss" betont, dass Gauss "den gesamten Beweisprozess unabhängig durchgeführt hat".

Während des Beweisprozesses hat es auch Detailsfehler in der ursprünglichen Dissertation entdeckt und korrigiert: In Prop 7 fehlte ein Minuszeichen bei der Berechnung der Funktion b(t), und es gab auch einen Defekt in einer Definition.

Das Forschungs-Team meint:

Die Verifikation eines Mathematik-Ergebnisses auf Fields-Medaille-Niveau zeigt, dass KI-Agenten wie Gauss bereits in der Lage sind, die Entwicklung der mathematischen Spitzenforschung zu beschleunigen.

Die Erweiterung des Maßstabs der automatischen Formalisierung wird das mathematische Wissenssystem und die Art der mathematischen Entdeckung grundlegend verändern, indem alle bekannten mathematischen Ergebnisse durchsuchbar gemacht werden.

Übrigens: Um diese formale Kenntnisse besser wartbar zu machen, haben die Forscher mit Hilfe von Gauss den Code automatisch neu strukturiert und optimiert, und die Anzahl der Codezeilen von einem Höchstwert von 500.000 auf etwa 200.000 reduziert.

Der Code wurde auf GitHub veröffentlicht.

Über Gauss

Der Gründer der Firma Math Inc., hinter der Gauss steht, ist Christian Szegedy, Mitbegründer von xAI und Autor von BatchNorm.

Er gründete 2025 Math, um mit KI "Mathematik zu lösen und alles zu lösen".

Bereits zuvor war Gauss berühmt geworden, als es in 3 Wochen die mathematische Herausforderung von Terence Tao und Alex Kontorovich - die Formalisierung des starken Primzahlsatzes (Prime Number Theorem, PNT) in Lean - abgeschlossen hatte.

Terence Tao selbst hat auch mit Math zusammengearbeitet, um explizite Schätzungen in der analytischen Zahlentheorie zu formalisieren und Argumente, die auf umfangreichen Berechnungen beruhen, in verifizierte, wiederverwendbare Bausteine umzuwandeln.

Damals gab es noch viele Zweifel an KI-Agenten wie Gauss, einschließlich des Grades der Automatisierung und des Ignorierens der impliziten Ziele mathematischer Probleme... Aber jetzt, wie Christian Szegedy selbst sagt:

(Vor weniger als zwei Jahren) dachten Mathematiker, dass es noch viele Jahre dauern würde, bis Künstliche Intelligenz in der Lage wäre, bei derartigen mathematischen Formalisierungsarbeiten (Formalisierung von Mathematik-Ergebnissen auf Fields-Medaille-Niveau) zu helfen.

Aber "Silizium-Gauss" hat heute einen neuen Durchbruch erzielt.

Referenzlinks:

[1]https://x.com/mathematics_inc/status/2028542388717986135

[2]https://www.math.inc/sphere-packing

Dieser Artikel stammt aus dem WeChat-Account "Quantum Bit", Autor: Yuyang. Veröffentlicht von 36Kr mit Genehmigung.