Thomas C. Hales

Publication Activity (10 Years)

Years Active: 1993-2020
Publications (10 Years): 2

Top Topics

Linear Inequalities

Automated Verification

Top Venues

NASA Formal Methods

Publications

Thomas C. Hales, Rodrigo Raya
Formal Proof of the Group Law for Edwards Elliptic Curves. IJCAR (2) (2020)
Thomas C. Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason M. Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, Roland Zumkeller
A formal proof of the Kepler conjecture. CoRR (2015)
Thomas C. Hales
Developments in Formal Proofs. CoRR (2014)
Alexey Solovyev, Thomas C. Hales
Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations. NASA Formal Methods (2013)
Alexey Solovyev, Thomas C. Hales
Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations CoRR (2013)
Thomas C. Hales
External Tools for the Formal Proof of the Kepler Conjecture. PxTP@CADE (2013)
Alexey Solovyev, Thomas C. Hales
Efficient Formal Verification of Bounds of Linear Programs. Calculemus/MKM (2011)
Thomas C. Hales
Linear Programs for the Kepler Conjecture - (Extended Abstract). ICMS (2010)
Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, Roland Zumkeller
A Revision of the Proof of the Kepler Conjecture. Discret. Comput. Geom. 44 (1) (2010)
Thomas C. Hales
Computational Discrete Geometry. ICMS (2010)
Thomas C. Hales
The Jordan Curve Theorem, Formally and Informally. Am. Math. Mon. 114 (10) (2007)
Thomas C. Hales
Some Methods of Problem Solving in Elementary Geometry. LICS (2007)
Thomas C. Hales
Historical Overview of the Kepler Conjecture. Discret. Comput. Geom. 36 (1) (2006)
Thomas C. Hales
Equidecomposable Quadratic Regions. Automated Deduction in Geometry (2006)
Thomas C. Hales
Sphere Packings, VI. Tame Graphs and Linear Programs. Discret. Comput. Geom. 36 (1) (2006)
Thomas C. Hales, Samuel P. Ferguson
A Formulation of the Kepler Conjecture. Discret. Comput. Geom. 36 (1) (2006)
Thomas C. Hales
Sphere Packing, III. Extremal Cases. Discret. Comput. Geom. 36 (1) (2006)
Thomas C. Hales
Sphere Packing, IV. Detailed Bounds. Discret. Comput. Geom. 36 (1) (2006)
Thomas C. Hales
Introduction to the Flyspeck Project. Mathematics, Algorithms, Proofs (2005)
Thomas C. Hales
Formalizing the Proof of the Kepler Conjecture. TPHOLs (2004)
Thomas C. Hales
Sphere packings and generative. SCG (2001)
Thomas C. Hales
The Honeycomb Conjecture. Discret. Comput. Geom. 25 (1) (2001)
Thomas C. Hales
Sphere Packings, I. Discret. Comput. Geom. 17 (1) (1997)
Thomas C. Hales
Sphere Packings, II. Discret. Comput. Geom. 18 (2) (1997)
Thomas C. Hales
Remarks on the density of sphere packings in three dimensions. Comb. 13 (2) (1993)