Flyspeck II: the basic linear programs

Steven Obua and Tobias Nipkow

We present another step, Flyspeck II, towards a complete, formal and mechanized proof of the Kepler Conjecture.

Springer online

BibTeX:

@article{ObuaN,author={Steven Obua and Tobias Nipkow},
title={Flyspeck {II}: The Basic Linear Programs},
journal={Annals of Mathematics and Artificial Intelligence},
volume=56,year=2009,pages={245-272}}