Thomas Callister Hales (born June 4, 1958) is an American

mathematician A mathematician is someone who uses an extensive knowledge of mathematics in their work, typically to solve mathematical problems. Mathematicians are concerned with numbers, data, quantity, structure, space, models, and change. History O ...

working in the areas of

representation theory Representation theory is a branch of mathematics that studies abstract algebraic structures by ''representing'' their elements as linear transformations of vector spaces, and studies modules over these abstract algebraic structures. In essen ...

discrete geometry Discrete geometry and combinatorial geometry are branches of geometry that study combinatorial properties and constructive methods of discrete geometric objects. Most questions in discrete geometry involve finite or discrete sets of basic geome ...

, and

formal verification In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal meth ...

. In

he is known for his work on the

Langlands program In representation theory and algebraic number theory, the Langlands program is a web of far-reaching and influential conjectures about connections between number theory and geometry. Proposed by , it seeks to relate Galois groups in algebraic ...

and the proof of the

fundamental lemma In mathematics, a fundamental theorem is a theorem which is considered to be central and conceptually important for some topic. For example, the fundamental theorem of calculus gives the relationship between differential calculus and integral calcu ...

over the group Sp(4) (many of his ideas were incorporated into the final proof of the fundamental lemma, due to

Ngô Bảo Châu Ngô Bảo Châu (, born June 28, 1972) is a Vietnamese-French mathematician at the University of Chicago, best known for proving the fundamental lemma for automorphic forms (proposed by Robert Langlands and Diana Shelstad). He is the first Vie ...

). In

, he settled the

Kepler conjecture The Kepler conjecture, named after the 17th-century mathematician and astronomer Johannes Kepler, is a mathematical theorem about sphere packing in three-dimensional Euclidean space. It states that no arrangement of equally sized spheres filling ...

on the density of sphere packings and the

honeycomb conjecture The honeycomb conjecture states that a regular hexagonal grid or honeycomb has the least total perimeter of any subdivision of the plane into regions of equal area. The conjecture was proven in 1999 by mathematician Thomas C. Hales. Theorem Let ...

. In 2014, he announced the completion of the Flyspeck Project, which formally verified the correctness of his proof of the

Biography

He received his Ph.D. from

Princeton University Princeton University is a private research university in Princeton, New Jersey. Founded in 1746 in Elizabeth as the College of New Jersey, Princeton is the fourth-oldest institution of higher education in the United States and one of the nin ...

in 1986, his dissertation was titled ''The Subregular Germ of Orbital Integrals''. Hales taught at

Harvard University Harvard University is a private Ivy League research university in Cambridge, Massachusetts. Founded in 1636 as Harvard College and named for its first benefactor, the Puritan clergyman John Harvard, it is the oldest institution of higher le ...

and the

University of Chicago The University of Chicago (UChicago, Chicago, U of C, or UChi) is a private research university in Chicago, Illinois. Its main campus is located in Chicago's Hyde Park neighborhood. The University of Chicago is consistently ranked among the be ...

, and from 1993 and 2002 he worked at the

University of Michigan , mottoeng = "Arts, Knowledge, Truth" , former_names = Catholepistemiad, or University of Michigania (1817–1821) , budget = $10.3 billion (2021) , endowment = $17 billion (2021)As o ...

. In 1998, Hales submitted his paper on the computer-aided

proof Proof most often refers to: * Proof (truth), argument or sufficient evidence for the truth of a proposition * Alcohol proof, a measure of an alcoholic drink's strength Proof may also refer to: Mathematics and formal logic * Formal proof, a con ...

of the

; a centuries-old problem in

which states that the most space-efficient way to pack spheres is in a tetrahedron shape. He was aided by graduate student Samuel Ferguson. In 1999, Hales proved the

, he also stated that the conjecture may have been present in the minds of mathematicians before

Marcus Terentius Varro Marcus Terentius Varro (; 116–27 BC) was a Roman polymath and a prolific author. He is regarded as ancient Rome's greatest scholar, and was described by Petrarch as "the third great light of Rome" (after Vergil and Cicero). He is sometimes call ...

. After 2002, Hales became the

University of Pittsburgh The University of Pittsburgh (Pitt) is a public state-related research university in Pittsburgh, Pennsylvania. The university is composed of 17 undergraduate and graduate schools and colleges at its urban Pittsburgh campus, home to the univers ...

's Mellon Professor of Mathematics. In 2003, Hales started work on Flyspeck to vindicate his proof of the Kepler conjecture. His proof relied on computer calculation to verify conjectures. The project used two

proof assistant In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor ...

HOL Light HOL Light is a member of the HOL theorem prover family. Like the other members, it is a proof assistant for classical higher order logic. Compared with other HOL systems, HOL Light is intended to have relatively simple foundations. HOL Light is a ...

and

Isabelle Isabel is a female name of Spanish origin. Isabelle is a name that is similar, but it is of French origin. It originates as the medieval Spanish form of '' Elisabeth'' (ultimately Hebrew '' Elisheva''), Arising in the 12th century, it became popu ...

. ''

Annals of Mathematics The ''Annals of Mathematics'' is a mathematical journal published every two months by Princeton University and the Institute for Advanced Study. History The journal was established as ''The Analyst'' in 1874 and with Joel E. Hendricks as the ...

'' accepted the proof in 2005; but was only 99% sure of the proof. In August 2014, the Flyspeck team's software finally verified the proof to be correct. 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. The goal of this project is to benefit from the increased precision and interoperability that computer formalisation provides while circumventing the effort that a full-scale formalisation of all published proofs currently entails. In the long term, the project hopes to build a corpus of mathematical facts which would allow for the application of machine learning techniques in interactive and automated theorem proving.

Awards and memberships

Hales won the

Chauvenet Prize The Chauvenet Prize is the highest award for mathematical expository writing. It consists of a prize of $1,000 and a certificate, and is awarded yearly by the Mathematical Association of America in recognition of an outstanding expository article ...

in 2003 and a

Lester R. Ford Award Lester is an ancient Anglo-Saxon surname and given name. Notable people and characters with the name include: People Given name * Lester Bangs (1948–1982), American music critic * Lester W. Bentley (1908–1972), American artist from Wisco ...

in 2008. In 2012 he became a fellow of the

American Mathematical Society The American Mathematical Society (AMS) is an association of professional mathematicians dedicated to the interests of mathematical research and scholarship, and serves the national and international community through its publications, meetings, ...

. He was invited to give the

Tarski Lectures The Alfred Tarski Lectures are an annual distinction in mathematical logic and series of lectures held at the University of California, Berkeley. Established in tribute to Alfred Tarski on the fifth anniversary of his death, the award has been give ...

in 2019; his three lectures were titled "A formal proof of the Kepler conjecture", "Formalizing mathematics", and "Integrating with Logic".

Publications

* * * * * * *

Notes

External links

* {{DEFAULTSORT:Hales, Thomas Callister 20th-century American mathematicians 21st-century American mathematicians 1958 births Living people University of Michigan faculty Princeton University alumni Scientists from Pittsburgh University of Pittsburgh faculty Fellows of the American Mathematical Society People from San Antonio Mathematicians from Texas Tarski lecturers