Lean-Beweis: Optimale Packung von 11 Quadraten formal verifiziert
AI-assisted proof of optimal packing for 11 squares
Die vollständige Optimalität der Packung von 11 Quadraten wurde in Lean formalisiert und verifiziert. Der Beweis umfasst 7.920 lokale Lean-Module und nutzt native numerische Zertifikate. Die optimale Seitenlänge beträgt etwa 3,8770835900228141773. Die Verifikation stützt sich auf den Lean-Kernel und den nativen Compiler, nicht nur auf den Kernel. Der Code und die Build-Konfiguration sind im Repository verfügbar.
Der vollständige Optimalitätsbeweis bestand die Verifikation mit nativen numerischen Zertifikaten.
- golden-face
Ich habe eine ganze Weile gebraucht, um zu verstehen, was Square Packing wirklich bedeutet (das Wiki ist aufschlussreich), aber TL;DR: Es geht darum, Einheitsquadrate (1x1) in ein größeres, beliebig dimensioniertes Quadrat zu packen. Wenn die Seitenlänge des größeren Quadrats keine ganze Zahl ist, wird es nicht trivial, die maximale Anzahl von 1x1-Quadraten zu bestimmen, die hineinpassen bzw. gepackt werden können.
- DevelopingElk
Ich arbeite an einer Reproduktion des Beweises mit einigen persönlichen Änderungen. Der grundlegende Ansatz ist der übliche computergestützte "unavoidable set"-Ansatz. Zuerst wählt man einige Regionen, die klein genug sind, dass zwei Quadratmittelpunkte nicht in dieselbe Region passen; der Artikel verwendete 16. Jede Region muss ein Quadrat enthalten oder nicht, was 16 choose 11 Fälle ergibt, etwa 2000. Für jeden Fall versucht man, ihn auszuschließen. Das macht man, indem man Bereiche identifiziert, die von einem Quadrat bedeckt sein müssen, und diese Information propagiert. Man kann auch Packungs-LPs verwenden, wie Stromquist es 1989 tat, um weitere Konfigurationen auszuschließen. Dann grenzt man die verbleibenden Fälle ein und unterteilt sie weiter.
Ich denke, der einzige Grund, warum das nicht schon vor der KI gemacht wurde, war, dass es kein Thema von ernsthaftem Interesse war. Die Computer von 1989 waren zu schwach, um alle Fälle zu bewältigen. Aber alle grundlegenden Zutaten waren im Beweis der Kepler-Vermutung vorhanden. Was die KI getan hat, war, den Aufwand so weit zu senken, dass Amateure, die einfach Quadratpackungen mochten, einen solchen Beweis durchführen und formal verifizieren konnten. Ich zähle mich selbst zu solchen Amateuren. Das ist also kein Fall, in dem KI Mathematikern Beweise stiehlt oder etwas Übermenschliches tut, sondern ein Fall von Demokratisierung. Ich mache mir Sorgen darüber, wie KI die Mathematik beeinflusst und wie sich die KI-Unternehmen verhalten, aber das ist nicht der Fall, über den man sich Sorgen machen sollte. Die Berechnungen zum Beweis, dass diese Anordnung optimal ist, werden immer zu groß sein, um sie von Hand zu überprüfen. Allerdings hoffe ich, einige schöne Visualisierungen des Packungs-LP oder der Kernüberlappung zu erstellen […]
- dkural
Es ist nicht so willkürlich oder hässlich, wie es auf den ersten Blick scheinen mag – siehe das Bild hier und die Erklärung: https://x.com/davidmbudden/status/2107646435659481548
- yzydserd
fwiw Die wichtigste Seite für Square-in-Square-Packing ist https://kingbird.myphotos.cc/packing/squares_in_squares.html
Die dreieckige Ansicht ist am interessantesten. Und ein 20-minütiges Video zu dieser Ansicht gibt es unter
- WithinReason
Eine Liste vieler Quadratpackungen, mit Bildern: