Introduction to the Flyspeck Project

Thomas C. Hales

Type: Article

Publication Date: 2006-01-01

Citations: 65

Locations

Dagstuhl Seminar Proceedings - View

Similar Works

Action	Title	Year	Authors
+	Introduction to the Flyspeck Project.	2005	Thomas C. Hales
+	Dense Sphere Packings: A Blueprint for Formal Proofs	2012	Thomas C. Hales
+	A formal proof of the Kepler conjecture	2015	Thomas Hales Mark Adams Gertrud Bauer Dat Tat Dang John Harrison Hoang Le Truong Cezary Kaliszyk Victor Magron Sean McLaughlin Thang Tat Nguyen
+	A formal proof of the Kepler conjecture	2015	Thomas Hales Mark Raymond Adams Gertrud Bauer Dat Tat Dang John Harrison Hoang Le Truong Cezary Kaliszyk Victor Magron S. McLaughlin Thang Tat Nguyen
+ PDF Chat	A FORMAL PROOF OF THE KEPLER CONJECTURE	2017	Thomas Hales Mark Adams Gertrud Bauer TAT DAT DANG John Harrison Hoang Le Truong Cezary Kaliszyk Victor Magron Sean McLaughlin TAT THANG NGUYEN
+ PDF Chat	The Formal Proof of the Kepler Conjecture: a critical retrospective	2024	Thomas Hales
+	A revision of the proof of the Kepler conjecture	2009	Thomas Hales John Harrison Sean McLaughlin Tobias Nipkow Steven Obua Roland Zumkeller
+ PDF Chat	External Tools for the Formal Proof of the Kepler Conjecture	2018	Thomas C. Hales
+	On a Detail in Hales's "Dense Sphere Packings: A Blueprint for Formal Proofs"	2017	Nadja Scharf
+	On a Detail in Hales's "Dense Sphere Packings: A Blueprint for Formal Proofs"	2017	Nadja Scharf
+	Dense Sphere Packings	2012	Thomas C. Hales
+	An overview of the Kepler conjecture	1998	Thomas C. Hales
+	The Kepler conjecture	1998	Thomas C. Hales
+	The Kepler conjecture	1998	Thomas Hales
+	A computer verification of the Kepler conjecture	2003	Thomas Hales
+	Linear Programs for the Kepler Conjecture	2010	Thomas Hales
+ PDF Chat	Historical Overview of the Kepler Conjecture	2006	Thomas Hales
+ PDF Chat	Book Review: Dense sphere packings: a blueprint for formal proofs	2015	Jeffrey C. Lagarias
+ PDF Chat	A Formulation of the Kepler Conjecture	2006	Thomas Hales Samuel P. Ferguson
+	Formalizing the Proof of the Kepler Conjecture	2004	Thomas Hales

Works That Cite This (33)

Action	Title	Year	Authors
+ PDF Chat	Certification of inequalities involving transcendental functions: Combining SDP and max-plus approximation	2013	Xavier Allamigeon Stéphane Gaubert Victor Magron Benjamin Werner
+	Ordered geometry in Hilbert's Grundlagen der Geometrie	2015	Phil Scott
+	Automated generation of machine verifiable and readable proofs: A case study of Tarski’s geometry	2015	Sana Stojanović Julien Narboux Predrag Janičić
+ PDF Chat	Certification of Bounds of Non-linear Functions: The Templates Method	2013	Xavier Allamigeon Stéphane Gaubert Victor Magron Benjamin Werner
+	From informal to formal proofs in Euclidean geometry	2018	Sana Stojanović
+ PDF Chat	The Area Method	2010	Predrag Janičić Julien Narboux Pedro Quaresma
+	The HOL Light Theory of Euclidean Space	2012	John Harrison
+	A Revision of the Proof of the Kepler Conjecture	2011	Thomas Hales John Harrison Sean McLaughlin Tobias Nipkow Steven Obua Roland Zumkeller
+ PDF Chat	A FORMAL PROOF OF THE KEPLER CONJECTURE	2017	Thomas Hales Mark Adams Gertrud Bauer TAT DAT DANG John Harrison Hoang Le Truong Cezary Kaliszyk Victor Magron Sean McLaughlin TAT THANG NGUYEN
+	A Revision of the Proof of the Kepler Conjecture	2009	Thomas Hales John Harrison Sean McLaughlin Tobias Nipkow Steven Obua Roland Zumkeller

Works Cited by This (8)

Action	Title	Year	Authors
+	Euclidean and Non-Euclidean Geometry: An Analytic Approach	1986	Patrick J. Ryan
+	An overview of the Kepler conjecture	1998	Thomas C. Hales
+	The Jordan-Schonflies Theorem and the Classification of Surface	1992	Carsten Thomassen
+ PDF Chat	Sphere packings, I	1997	Thomas Hales
+ PDF Chat	Bounds for Local Density of Sphere Packings and the Kepler Conjecture	2002	Jeffrey C. Lagarias
+ PDF Chat	Theory on plane curves in non-metrical analysis situs	1905	Oswald Veblen
+ PDF Chat	A proof of the Kepler conjecture	2005	Thomas Hales
+ PDF Chat	The Kissing Problem in Three Dimensions	2005	Oleg R. Musin