Thomas Hales (born 1958) is an American mathematician best known for proving the Kepler Conjecture, the nearly four-century-old claim that no packing of equal spheres in space is denser than cubic or hexagonal close packing. Hales announced a computer-assisted proof in 1998, following an approach suggested by Laszlo Fejes Toth; because the proof relied on extensive computation, it was not fully machine-verified until 2014, when the Flyspeck project he led completed a formal proof using the Isabelle and HOL Light proof assistants, later accepted for publication in 2017. He also proved the honeycomb conjecture in 1999 and, in 2017, initiated the Formal Abstracts project to encode the results of mathematical papers in machine-checkable form. This description is adapted from Wikipedia contributors under CC BY-SA 4.0; changes were made. https://creativecommons.org/licenses/by-sa/4.0/
Facts
BirthplaceSan Antonio, Texas, United States 1 Nationality / Culture Defining ContributionAnnounced a computer-assisted proof of the Kepler Conjecture in 1998, following an approach suggested by Laszlo Fejes Toth in 1953. 2 Defining ContributionInitiated the Formal Abstracts project in 2017, aiming to encode the main results of mathematical research papers as formalised statements in the language of an interactive theorem prover. 1 Defining ContributionLed the Flyspeck project, which in August 2014 completed a formal, machine-checked verification of the Kepler Conjecture proof using the Isabelle and HOL Light proof assistants. 1 Notable WorkFormal proof of the Kepler Conjecture (Flyspeck project, completed 2014) 1 AwardChauvenet Prize (2003); Fulkerson Prize (2009); Fellow of the American Mathematical Society (2012). 1 Connections
In Branch
Proved the Kepler conjecture on sphere-packing density (1998, formally verified 2014) and the honeycomb and dodecahedral conjectures, all discrete geometry results.
Source Thomas Hales (Wikipedia)
Proofs Credited
Hales announced a proof in 1998; the Flyspeck project completed a formal machine-verified proof in 2014, accepted for publication in 2017.
Source Kepler Conjecture (Wikipedia)
In the Other Atlases
Sources
1. Thomas Hales (Wikipedia)
Wikimedia FoundationBiography section
In 2017, he initiated the Formal Abstracts project which aims to provide formalised statements of the main results of each mathematical research paper in the language of an interactive theorem prover.
Infobox
Born (1958-06-04) June 4, 1958 (age 68) San Antonio, Texas ... Known for Proof of the Kepler conjecture Proof of the honeycomb conjecture Proof of the dodecahedral conjecture
Lead section
Thomas Callister Hales is an American mathematician working in the areas of representation theory, discrete geometry, and formal verification. In discrete geometry, he settled the Kepler conjecture on the density of sphere packings, the honeycomb conjecture, and the dodecahedral conjecture. In 2014, he announced the completion of the Flyspeck Project, which formally verified the Kepler conjecture proof.
Awards section
Awards Chauvenet Prize (2003) Moore Prize (2004) David P. Robbins Prize (2007) Lester R. Ford Award (2008) Fulkerson Prize (2009) Tarski Lectures (2019) Senior Berwick Prize (2020)
Lead section, gender reference
In representation theory he is known for his work on the Langlands program and the proof of the fundamental lemma over the group Sp(4).
View the Source 2. Kepler Conjecture (Wikipedia)
Wikimedia FoundationHales' proof sectionQuote, Hales' proof section
In 1998, the American mathematician Thomas Hales, following an approach suggested by Fejes Toth (1953), announced that he had a proof of the Kepler conjecture.
Reader Challenges (0)
No disputes yet. Spotted an error or a better source? Open the first one.
Sign in to dispute this or suggest a correction.