We stand with Ukraine  

Thomas C. Hales

According to our database1, Thomas C. Hales authored at least 25 papers between 1993 and 2020.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2020
Formal Proof of the Group Law for Edwards Elliptic Curves.
[BibTeX]
[DOI]
Thomas C. Hales
,
Rodrigo Raya
Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2015
A formal proof of the Kepler conjecture.
[BibTeX]
[DOI]
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
CoRR, 2015

2014
Developments in Formal Proofs.
[BibTeX]
[DOI]
Thomas C. Hales
CoRR, 2014

Mathematics in the age of the Turing machine.
[BibTeX]
[DOI]
Thomas C. Hales
Proceedings of the Turing's Legacy: Developments from Turing's Ideas in Logic, 2014

2013
Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations.
[BibTeX]
[DOI]
Alexey Solovyev
,
Thomas C. Hales
Proceedings of the NASA Formal Methods, 2013

External Tools for the Formal Proof of the Kepler Conjecture.
[BibTeX]
[DOI]
Thomas C. Hales
Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

2011
Efficient Formal Verification of Bounds of Linear Programs.
[BibTeX]
[DOI]
Alexey Solovyev
,
Thomas C. Hales
Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

2010
A Revision of the Proof of the Kepler Conjecture.
[BibTeX]
[DOI]
Thomas C. Hales
,
John Harrison
,
Sean McLaughlin
,
Tobias Nipkow
,
Steven Obua
,
Roland Zumkeller
Discret. Comput. Geom., 2010

Linear Programs for the Kepler Conjecture - (Extended Abstract).
[BibTeX]
[DOI]
Thomas C. Hales
Proceedings of the Mathematical Software, 2010

Computational Discrete Geometry.
[BibTeX]
[DOI]
Thomas C. Hales
Proceedings of the Mathematical Software, 2010

2007
The Jordan Curve Theorem, Formally and Informally.
[BibTeX]
[DOI]
Thomas C. Hales
Am. Math. Mon., 2007

Some Methods of Problem Solving in Elementary Geometry.
[BibTeX]
[DOI]
Thomas C. Hales
Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 2007

2006
A Formulation of the Kepler Conjecture.
[BibTeX]
[DOI]
Thomas C. Hales
,
Samuel P. Ferguson
Discret. Comput. Geom., 2006

Sphere Packings, VI. Tame Graphs and Linear Programs.
[BibTeX]
[DOI]
Thomas C. Hales
Discret. Comput. Geom., 2006

Sphere Packing, IV. Detailed Bounds.
[BibTeX]
[DOI]
Thomas C. Hales
Discret. Comput. Geom., 2006

Sphere Packing, III. Extremal Cases.
[BibTeX]
[DOI]
Thomas C. Hales
Discret. Comput. Geom., 2006

Historical Overview of the Kepler Conjecture.
[BibTeX]
[DOI]
Thomas C. Hales
Discret. Comput. Geom., 2006

Equidecomposable Quadratic Regions.
[BibTeX]
[DOI]
Thomas C. Hales
Proceedings of the Automated Deduction in Geometry, 2006

2005
Introduction to the Flyspeck Project.
[BibTeX]
[DOI]
Thomas C. Hales
Proceedings of the Mathematics, Algorithms, Proofs, 9.-14. January 2005, 2005

2004
Formalizing the Proof of the Kepler Conjecture.
[BibTeX]
[DOI]
Thomas C. Hales
Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

2001
The Honeycomb Conjecture.
[BibTeX]
[DOI]
Thomas C. Hales
Discret. Comput. Geom., 2001

Sphere packings and generative.
[BibTeX]
[DOI]
Thomas C. Hales
Proceedings of the Seventeenth Annual Symposium on Computational Geometry, 2001

1997
Sphere Packings, I.
[BibTeX]
[DOI]
Thomas C. Hales
Discret. Comput. Geom., 1997

Sphere Packings, II.
[BibTeX]
[DOI]
Thomas C. Hales
Discret. Comput. Geom., 1997

1993
Remarks on the density of sphere packings in three dimensions.
[BibTeX]
[DOI]
Thomas C. Hales
Comb., 1993


  Loading...