English

On a Detail in Hales's "Dense Sphere Packings: A Blueprint for Formal Proofs"

Metric Geometry 2017-12-12 v1

Abstract

In "Dense Sphere Packings: A Blueprint for Formal Proofs" Hales proves that for every packing of unit spheres, the density in a ball of radius rr is at most π/18+c/r\pi/\sqrt{18}+c/r for some constant cc. When rr tends to infinity, this gives a proof to the famous Kepler conjecture. As formulated by Hales, cc depends on the packing. We follow the proofs of Hales to calculate a constant cc' independent of the sphere packing that exists as mentioned in "A Formal Proof of the Kepler Conjecture" by Hales et al..

Keywords

Cite

@article{arxiv.1712.03568,
  title  = {On a Detail in Hales's "Dense Sphere Packings: A Blueprint for Formal Proofs"},
  author = {Nadja Scharf},
  journal= {arXiv preprint arXiv:1712.03568},
  year   = {2017}
}