Tobias Nipkow
TU Munich

``Towards a machine-checked proof of the enumeration of tame plane graphs"

Abstract:

Hales' proof of the Kepler conjecture defines a class of tame plane graphs, enumerates that class by computer and checks (again by computer) that none of these graphs constitute a counterexample to the conjecture. This talk reports on work in progress to verify that Hales' program for enumerating tame plane graphs is correct, i.e. does not miss any such graph. This is part of Hales' Flyspeck project to check his whole proof by computer. After a brief introduction to tame graphs and their role in Hales' proof, the enumeration procedure is explained, and its correctness proof its sketched. Throughout the talk we concentrate on the issues that arise when checking mathematical arguments by machine, in particular the challenge of writing programs that are both efficient enough to perform complex searches and enumerations but simple enough that machine-checked correctness proofs become feasible. This work was done while visiting the University of Pittsburgh and builds on the PhD thesis by Gertrud Bauer.

Back to Talks Page