Formal Global Optimisation with Taylor Models. - Roland Zumkeller (IJCAR, 2006)

A Revision of the Proof of the Kepler Conjecture. - Thomas C. Hales; John Harrison 001; Sean McLaughlin; Tobias Nipkow; Steven Obua; Roland Zumkeller (Discret. Comput. Geom., 2010)

A formal proof of the Kepler conjecture. - Thomas C. Hales; Mark Adams; Gertrud Bauer; Dat Tat Dang; John Harrison 001; Truong Le Hoang; Cezary Kaliszyk; Victor Magron; Sean McLaughlin; Thang Tat Nguyen; Truong Quang Nguyen; Tobias Nipkow; et al. (CoRR, 2015)