Exakte Arithmetik für reelle Zahlen als Basis für einen maschinellen Beweis der Keplerschen Vermutung
Final Report Abstract
Die fast 400 Jahre alte Keplersche Vermutung besagte, dass die optimale Packungsdichte von 3-dimensionalen Kugeln gleicher Gr¨oße ¼ 3p2 ist. Sie wurde 1998 von Thomas Hales bewiesen. Allerdings mit erheblicher Hilfe durch unverifizierte Berechnungen, weshalb die Gutachter diese Teile des Beweises nicht ¨uberpr¨ufen konnten. Thomas Hales hat daraufhin ein informelles internationales Projekt Flyspeck ins Leben gerufen, um die auf Berechnungen beruhenden Teile des Beweises mit Hilfe maschineller Theorembeweiser zu ¨uberpr¨ufen. Wir haben zwei Teile des Beweises im Theorembeweiser Isabelle/HOL formalisiert und verifiziert: • Die Generierung der fast 2771 m¨oglichen Gegenbeispiele als Graphen. • Die ¨Uberpr¨ufung, dass keiner der Graphen eine r¨aumliche Konfiguration beschreibt, die eine gr¨oßere Packungsdichte hat als ¼ 3p2 . Leider konnten aus Zeitgr¨unden bis Projektende nur f¨ur 2565 der 2771 Konfigurationen dieser Nachweis erbracht werden. Dies geschah vollautomatisch. Die restlichen 206 Graphen mussten auch von Hales mit speziellen Methoden und teilweise von Hand bearbeitet werden, um die lineare Optimierung anwenden zu k¨onnen. Technisch haben wir folgende Fortschritte erzielt: • Wir haben eine von Flyspeck unabh¨angige Methode entwickelt und in Isabelle/HOL implementiert, wie man die unverifizierten Ergebnisse eines externen Linearen Optimierers in einem Theorembeweiser zertifizieren kann. Damit kann man im Prinzip beliebig genaue Approximationen der tats¨achlichen optimalen L¨osung verifizieren. • Wir haben in Isabelle/HOL ein Beweismethode implementiert, die Ungleichungen zwischen reellwertigen Termen beweisen kann, wenn die Werte aller Variablen innerhalb fixer Grenzen liegen, etwa 1 · x · 3 =) ln x < 1.1515 • Wir haben das HOL Light System von John Harrison um die Generierung von Beweistermen erweitert, die wir dann in Isabelle/HOL importieren k¨onnen. Dies ist notwendig, da andere Teile des Flyspeck Projekts in HOL Light bewiesen werden, z.B. die Beitr¨age von Hales und Harrison.
Publications
- Steven Obua and Sebastian Skalberg. Importing HOL into Isabelle/HOL. In: Automated Reasoning (IJCAR 2006).
- Steven Obua. Checking Conservativity of Overloaded Definitions in Higher-Order Logic. In: Term Rewriting and Applications (RTA 2006).
- Steven Obua. Partizan Games in Isabelle/HOLZF. In: Theoretical Aspects of Computing (ICTAC 2006).
- Steven Obua. Proof Pearl: Looping Around the Orbit. In: Theorem Proving in Higher Order Logics (TPHOLs 2007).
- Steven Obua. Proving Bounds for Real Linear Programs in Isabelle/ HOL. In: Theorem Proving in Higher Order Logics (TPHOLs 2005).
- Tobias Nipkow, Gertrud Bauer, Paula Schultz. Flyspeck I: Tame Graphs. In: Automated Reasoning (IJCAR 2006).
