Thomas C. Hales

26 papers A* 1Journal 14Unranked 10
YearRankTypeTitle / Venue / Authors
2020 — conf
Formal Proof of the Group Law for Edwards Elliptic Curves.
IJCAR (2)
Thomas C. Hales, Rodrigo Raya
2015 J jnl
A formal proof of the Kepler conjecture.
CoRR
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
2014 J jnl
Developments in Formal Proofs.
CoRR
Thomas C. Hales
2014 — ch.
Mathematics in the age of the Turing machine.
Turing's Legacy
Thomas C. Hales
2013 — conf
External Tools for the Formal Proof of the Kepler Conjecture.
PxTP@CADE
Thomas C. Hales
2013 J jnl
Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations
CoRR
Alexey Solovyev, Thomas C. Hales
2013 — conf
Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations.
NASA Formal Methods
Alexey Solovyev, Thomas C. Hales
2011 — conf
Efficient Formal Verification of Bounds of Linear Programs.
Calculemus/MKM
Alexey Solovyev, Thomas C. Hales
2010 J jnl
A Revision of the Proof of the Kepler Conjecture.
Discret. Comput. Geom.
Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, Roland Zumkeller
2010 — conf
Computational Discrete Geometry.
ICMS
Thomas C. Hales
2010 — conf
Linear Programs for the Kepler Conjecture - (Extended Abstract).
ICMS
Thomas C. Hales
2007 A* conf
Some Methods of Problem Solving in Elementary Geometry.
LICS
Thomas C. Hales
2007 J jnl
The Jordan Curve Theorem, Formally and Informally.
Am. Math. Mon.
Thomas C. Hales
2006 J jnl
A Formulation of the Kepler Conjecture.
Discret. Comput. Geom.
Thomas C. Hales, Samuel P. Ferguson
2006 — conf
Equidecomposable Quadratic Regions.
Automated Deduction in Geometry
Thomas C. Hales
2006 J jnl
Historical Overview of the Kepler Conjecture.
Discret. Comput. Geom.
Thomas C. Hales
2006 J jnl
Sphere Packing, III. Extremal Cases.
Discret. Comput. Geom.
Thomas C. Hales
2006 J jnl
Sphere Packing, IV. Detailed Bounds.
Discret. Comput. Geom.
Thomas C. Hales
2006 J jnl
Sphere Packings, VI. Tame Graphs and Linear Programs.
Discret. Comput. Geom.
Thomas C. Hales
2005 — conf
Introduction to the Flyspeck Project.
Mathematics, Algorithms, Proofs
Thomas C. Hales
2004 — conf
Formalizing the Proof of the Kepler Conjecture.
TPHOLs
Thomas C. Hales
2001 — conf
Sphere packings and generative.
SCG
Thomas C. Hales
2001 J jnl
The Honeycomb Conjecture.
Discret. Comput. Geom.
Thomas C. Hales
1997 J jnl
Sphere Packings, I.
Discret. Comput. Geom.
Thomas C. Hales
1997 J jnl
Sphere Packings, II.
Discret. Comput. Geom.
Thomas C. Hales
1993 J jnl
Remarks on the density of sphere packings in three dimensions.
Comb.
Thomas C. Hales