Flyspeck II - The Basic Linear Programs

EPFL IC Tresor talks

by Steven Obua Formalization of the Proof of the Kelper Conjecture. Building on the work started in Flyspeck I, we continued the formalization of the proof of the Kepler Conjecture by eliminating further 92.5% of the tame graphs enumerated in Flyspeck I. This is done by showing that the basic linear program associated with an eliminated tame graph is infeasible. This work has been carried out using the Isabelle mechanical theorem prover which has been amended by the HOL Computing Library.