Thomas C. Hales
PhD, Princeton University
Mellon Professor, University of Pittsburgh
Email: MYLASTNAME AT PITT DOT EDU
Encryption Works! Fight surveillance!
Pitt Algebra, Combinatorics, and Geometry Research Group
- Endoscopic transfer of orbital integrals in large residual characteristic (with J. Gordon)
- The Formal Proof of the Kepler Conjecture (with many coauthors, including Hoang Le Truong and A. Solovyev). The project is officially complete.
- Bourbaki report on Developments in Formal Proofs (pdf) (youtube)
- (with A. Solovyev) Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations, 2012
- A Proof of Fejes Toth's Conjecture on Sphere Packings with Kissing Number Twelve
- Mathematics in the Age of the Turing Machine (survey paper on computers in mathematics, Lecture Notes in Logic (CUP) in commemoration of the centennial of Turing's birth)
- On the Reinhardt Conjecture (Vietnam Journal of Mathematics)
- Dense Sphere Packings: a blueprint for formal proofs (book, Cambridge University Press, available on Amazon), errata
- The Strong Dodecahedral Conjecture and Fejes Toth's Conjecture on Sphere Packings with Kissing Number Twelve, (arXiv preprint, to appear Fields Institute, 2013)
- (with A. Solovyev) Efficient formal verification of bounds of linear programs, in LNCS 6824
Research (Representation theory, formal proofs, motivic integration, discrete geometry)
- The Kepler Conjecture (What is the densest arrangement of spheres in space?)
- Flyspeck Project Page (the Formal Proof of the Kepler Conjecture)
Join The Boycott of Elsevier
"Don't use manual procedures" -Andrew Hunt and David Thomas and ... "don't rely on social processes for verification" -David Dill
License This site is licensed under creative commons. Help yourself!