In 1998, Thomas Hales published a proof of the Kepler Conjecture, which states that the {\em cubic close packing} is the densest possible packing of equally-sized spheres. The proof is by exhaustion on a set of 3050 plane graphs satisfying certain properties, called {\em tame plane graphs}. The enumeration of this set has been generated by a computer program, hence the completeness of this enumeration is essential for the proof. In this thesis, we formalize a theory of plane graphs defined as an inductive set in the theorem prover Isabelle/HOL: a plane graph is constructed starting with one face and repeatedly adding new faces. Based on this theory, we formalize one part of the proof of the Kepler Conjecture, the completeness of the enumeration of tame plane graphs.     «

In 1998, Thomas Hales published a proof of the Kepler Conjecture, which states that the {\em cubic close packing} is the densest possible packing of equally-sized spheres. The proof is by exhaustion on a set of 3050 plane graphs satisfying certain properties, called {\em tame plane graphs}. The enumeration of this set has been generated by a computer program, hence the completeness of this enumeration is essential for the proof. In this thesis, we formalize a theory of plane graphs defined as an...     »

Im Jahre 1998 veröffentlichte der Mathematiker Thomas Hales einen Beweis der auf Kepler zurückgehenden Vermutung, daß die kubisch dichte Kugelpackung (englisch {\em cubic close packing}) die dichteste Kugelpackung ist. Der Beweis beruht auf einer umfangreichen, durch ein Programm generierten Fallunterscheidung über ca. 3050 Fälle. Dabei wird jeder Fall durch einen ebenen Graphen mit bestimmten Eigenschaften, einem sogenannten {\em zahmen Graphen} repräsentiert. Wesentlich für den Beweis ist die Vollständigkeit dieser Aufzählung. In dieser Arbeit geht es um eine Formalisierung einer Theorie ebener Graphen in dem Theorembeweiser Isabelle/HOL, basierend auf einer Definition als induktive Menge: Eine Konstruktion eines ebenen Graphen beginnt mit einer einzigen Fäche, an die sukzessive neue Flächen angelegt werden. Darauf aufbauend wird ein Teil des Beweises der Kepler Vermutung formalisiert, die Vollständigkeit der Aufzählung der zahmen Graphen.     «

Im Jahre 1998 veröffentlichte der Mathematiker Thomas Hales einen Beweis der auf Kepler zurückgehenden Vermutung, daß die kubisch dichte Kugelpackung (englisch {\em cubic close packing}) die dichteste Kugelpackung ist. Der Beweis beruht auf einer umfangreichen, durch ein Programm generierten Fallunterscheidung über ca. 3050 Fälle. Dabei wird jeder Fall durch einen ebenen Graphen mit bestimmten Eigenschaften, einem sogenannten {\em zahmen Graphen} repräsentiert. Wesentlich für den Beweis ist die...     »