collaborators

1 paper

math.MG2015

A formal proof of the Kepler conjecture

Thomas Hales, Mark Adams, Gertrud Bauer +19

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…