A FORMAL PROOF OF THE KEPLER CONJECTURE. (29th May 2017) - HALES, THOMAS
Abstract : This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project.