Thomas Callister Hales

14 languages

Tools

From Wikipedia, the free encyclopedia

Thomas Hales

Born

June 4, 1958

(age 67)

Alma mater

Known for

Proof of the

Awards

(2003)

(2004)

(2007)

(2008)

(2009)

(2019)

(2020)

Scientific career

Fields

Institutions

Doctoral

students

Thomas Callister Hales

(born June 4, 1958) is an American

working in the areas of

, and

. In

he is known for his work on the

and the proof of the

over the group

(many of his ideas were incorporated into the final proof of the fundamental

lemma, due to

, he settled the

on the density of

, the

, and

the

. 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

in 1986 with a dissertation

titled

The Subregular Germ of Orbital Integrals

Hales taught at

and the

and from 1993 and 2002 he worked

at the

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

of the

, a centuries-old problem in

which states that

the most space-efficient way to

is in a tetrahedron shape. He

was aided by graduate student Samuel Ferguson.

In 1999, Hales proved the

, and also stated that the conjecture may have been in

the minds of mathematicians before

. The conjecture is

mentioned by

in his Book V.

After 2002, Hales became the

'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

and

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

. 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.

Hales worked on a conjecture of

with Koundinya Vajjha, that

the

has the lowest maximum packing density of all centrally symmetric convex shapes in the plane.

Although they failed to prove Reinhardt's conjecture, in 2024 they claim to have proved

a related conjecture of

It seems highly probable from the convexity condition, that the boundary of an extreme convex domain consists

of line segments and arcs of hyperbolae.

Hales retired in May of 2025.

Awards

[

]

Hales was an invited speaker at the

in 2002.

He won the

2003,

the

in 2004,

in 2008,

and a

in 2009.

He was

awarded the inaugural

of the

in 2007.

In 2012 he became a fellow of the

He was invited to give the

in 2019. His three lectures were titled

"A formal proof of the Kepler conjecture", "Formalizing mathematics", and "Integrating with Logic".

He was

awarded the

of the

in 2020.

Publications

[

]

Hales, Thomas C. (1994).

(3):

47–

58.

Hales, Thomas C. (2001).

(1):

1–

22.

Hales, Thomas C. (2005).

162

(3):

1065–

1185.

Hales, Thomas C. (2006).

(1):

5–

20.

Hales, Thomas C.; Ferguson, Samuel P. (2006).

(1):

21–

69.

Hales, Thomas C.; Ferguson, Samuel P. (2011),

The Kepler Conjecture: The Hales-Ferguson Proof

, New York: Springer,

Hales, Thomas C.; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang, Truong Le; Kaliszyk, Cezary;

Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso,

Joseph; Rute, Jason; Solovyev, Alexey; An Hoai Thi Ta; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky;

Zumkeller, Roland (2017).

Forum of Mathematics, Pi

e2.

Notes

[

]

Hales, Thomas C. (1992).

(PDF)

Memoirs of the American Mathematical Society

(476).

. Archived from

(PDF)

on 2020-02-29.

. Archived from

on 2020-12-27.

. Archived from

on 2018-06-17

. Retrieved

2016-12-29

. Archived from

on 2011-09-27

. Retrieved

2016-12-29

2007-05-29 at the

The University Record

(University of Michigan), September 16, 1998

Aron, Jacob (August 12, 2014).

New Scientist

. Retrieved

May 10,

2017

Project website

, retrieved 2020-01-10.

Hales, Thomas; Vajjha, Koundinya (2024). "Packings of Smoothed Polygons".

[

(1947).

(PDF)

Proceedings of

the Koninklijke Nederlandse Academie van Wetenschappen

108–

118.

. University of Pittsburgh, Department of Mathematics

. Retrieved

2026-03-26

www.mathunion.org

. Retrieved

2024-10-13

Hales, Thomas C. (2000).

Notices of the AMS

(4):

440–

449.

www.reliable-computing.org

. Retrieved

2024-10-13

Hales, Thomas C. (2007).

114

(10):

882–

894.

American Mathematical Society

. Retrieved

2024-10-13

American Mathematical Society

. Retrieved

2024-10-13

, retrieved 2013-01-19.

math.berkeley.edu

. Retrieved

2021-11-02

logic.berkeley.edu

. Retrieved

2021-11-02

www.lms.ac.uk

. Retrieved

2024-10-13

External links

[

]

at the

International

National

Academics

People

Other

recipients

1925

1929

1932

1935

1938

1941

1944

1947

1950

1953

1956

1960

1963

1964

1965

and

1967

1968

1970

1971

1972

1973

1974

1975

and

1976

1977

1978

1979

1980

1981

1982 No award given.

1983 No

award given.

1984

1985

1986

1987

1988

1989

1990

1991

and

1992

1993

and

1994

1995

1996

1997

1998

and

1999

2000

2001

and

2002

, and

2003

2004

2005

2006

2007

2008

2009

2010

2011

2012

2013

2014

2015

2016

2017

2018

2019

2020

2021

2022

2023

2024

This page was last edited on 26 March 2026, at 08:41

(UTC)

Text is available under the

; additional terms may apply. By using this site, you agree to the

and

. Wikipedia® is a registered trademark of the

, a non-profit organization.