Dense Sphere Packings: A Blueprint for Formal Proofs

By T. Hales. 2012

98 citations recorded by the source corpus.

Subfields: Computer Graphics and Computer-Aided Design, Geometry and Topology, Theoretical Computer Science

View Paper: https://www.semanticscholar.org/paper/77f49bc592a28e623f4efede631e5493cf85174d

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computer Graphics and Computer-Aided Design

1. Josef Urban
2. John Harrison
3. Freek Wiedijk

In Geometry and Topology

1. Josef Urban
2. John Harrison
3. Freek Wiedijk

In Theoretical Computer Science

1. Josef Urban
2. John Harrison
3. Freek Wiedijk

Citations in the corpus

• History of Interactive Theorem Proving (2014, methodology): “An early effort in this direction is Hales’s cross-linking of his informal LATEX book on Flyspeck [Hales, 2012] with the formal Flyspeck development in HOL Light and a wiki platform for such joint informal/formal alignment [Tankink et al., 2013].”