A formal proof of the Kepler conjecture

Department of Computer Science