FÜNF KÖRPER, ENDLICH VIELE PERFEKTE TÄNZE

Man stelle sich einige Sterne oder Planeten vor, die so genau angeordnet sind, dass sich die ganze Gruppe wie ein starrer Gegenstand drehen kann, ohne ihre Form zu ändern. Dafür muss die Schwerkraft auf jeden Körper genau zum Schwerpunkt der Gruppe zeigen, mit einer Stärke proportional zu seinem Abstand davon. Solche Anordnungen heißen Zentralkonfigurationen. Sie sind die Formen jener besonderen Lösungen des n-Körper-Problems, bei denen die Körper dasselbe relative Muster beibehalten, einschließlich der relativen Gleichgewichte, die sich starr drehen.

Wenn ein Muster funktioniert, funktioniert auch jede gedrehte, vergrößerte oder verschobene Kopie davon; deshalb zählen Mathematiker sie „bis auf Ähnlichkeit“.

Smales sechstes Problem

Die Frage ist einfach formuliert: Ist die Anzahl der Zentralkonfigurationen für jede Wahl positiver Massen endlich? Es ist das sechste Problem auf einer Liste offener Probleme, die der Mathematiker Smale aufgestellt hat.

So war der Stand laut der Arbeit:

• Drei Körper: genau fünf – Lagranges zwei gleichseitige Dreiecke und Eulers drei gerade Linien.
• Vier Körper: Die Endlichkeit wurde von Hampton und Moeckel für alle positiven Massen bewiesen.
• Fünf Körper in einer Ebene: Albouy und Kaloshin bewiesen die Endlichkeit 2012, aber nur für Massen außerhalb einer Ausnahmemenge – einer dünnen, durch Polynomgleichungen definierten Familie von Massenkombinationen, bei der ihr Argument versagte.

Die Ausnahmemenge schließen

Tejasvi Singh Tomar beseitigt diese Ausnahmemenge. Der Hauptsatz: Für jede Wahl von fünf positiven Massen hat das ebene Fünfkörperproblem bis auf Ähnlichkeit endlich viele Zentralkonfigurationen.

Die Strategie folgt Albouy und Kaloshin. Gäbe es unendlich viele Konfigurationen, bildeten sie eine stetige Kurve von Lösungen, wenn man die Gleichungen auf komplexe Zahlen erweitert. Folgt man dieser Kurve „ins Unendliche“, müssen sich die Abstände zwischen den Körpern so verhalten, dass sie sich in einem genauen Gleichgewicht aufheben. Die Körper nähern sich einem von sechzehn Grenzdiagrammen, die Albouy und Kaloshin identifiziert haben und von denen jedes Bedingungen an die Massen stellt.

Die neue Arbeit macht diese Bedingungen für jede positive Masse scharf und schließt die schwierigen Fälle einen nach dem anderen aus:

• Konfigurationen, in denen vier Körper einen engen Haufen bilden, dem sich der fünfte nähert, werden ausgeschlossen, indem man die potenzielle Energie – die entlang der Kurve konstant bleibt – in immer höhere Ordnungen entwickelt; für positive Massen widersprechen sich die resultierenden Bedingungen;
• für zwei weitere Diagramme wird gezeigt, dass sie nie auftreten;
• für alles Übrige beschreibt der Autor alle verträglichen Massenbedingungen mit exakter Computeralgebra – 2.206 algebraische Systeme – und erzeugt für jedes ein numerisches Zertifikat: eine Liste rationaler Zahlen, deren Eigenschaften, in exakter Arithmetik geprüft, beweisen, dass das Gleichgewicht unmöglich ist.

Eine Falle durch negative Massen

Es gibt einen Haken, um den reine Algebra nicht herumkommt. Ein anderer Mathematiker, Roberts, hatte unendlich viele Zentralkonfigurationen für die Massen (1, 1, 1, 1, −¼) gefunden – mit einer negativen Masse. Durch Umdrehen einiger Vorzeichen wird daraus eine unendliche Menge von Lösungen der komplexifizierten Gleichungen für die Massen (4, 4, 4, 4, 1). Es sind keine echten Konfigurationen, doch ein Argument, das nur die komplexen Gleichungen sieht, kann sie nicht unterscheiden.

Daher zählt der Autor bei diesen Massen und beim verwandten Verhältnis (1, 1, 4, 4, 4) die echten Konfigurationen direkt, mit einer Computersuche, die garantierte Intervallarithmetik verwendet:

• für die Massen (1, 4, 4, 4, 4): 306 Konfigurationen bis auf Drehung und Skalierung – 60 auf einer Geraden, 24 als konvexes Fünfeck, die übrigen mit einem oder zwei Körpern im Inneren;
• für (1, 1, 4, 4, 4): 294.

Die 60 geradlinigen stimmen mit einer früheren Zählung von Moulton überein.

Von der Maschine geprüft

Ein Beweis, der auf so vielen Berechnungen beruht, braucht eine starke Überprüfung. Jedes Zertifikat wurde von einem separaten Programm, das nach den Definitionen der Arbeit geschrieben wurde, erneut geprüft. Vor allem ist der Satz im Beweisassistenten Lean 4 bewiesen, einem Programm, das jeden logischen Schritt prüft. Der formale Beweis setzt nicht einmal die Ergebnisse von Albouy und Kaloshin voraus: Er leitet das Nötige selbst her und findet per Suche 1.376 beschriftete Diagramme, die ihren Regeln genügen. Er wird von zwei weiteren unabhängigen Prüfprogrammen für Lean-Beweise akzeptiert. Ihn von Grund auf zu bauen, dauert etwa 860 CPU-Stunden.

Die Arbeit endet mit einer kurzen Erklärung: Generative KI-Werkzeuge wurden eingesetzt, um die Ergebnisse zu finden und zu beweisen, die Programme und die Lean-Formalisierung zu schreiben und den Text zu entwerfen. Die Werkzeuge werden nicht genannt.

Was es aussagt und was nicht

Das Ergebnis betrifft fünf Körper in einer Ebene. Es beweist, dass die Anzahl der Konfigurationen für jede Wahl positiver Massen endlich ist, liefert aber exakte Zahlen nur für die wenigen untersuchten Massenverhältnisse.