Thomas Callister Hales Mellon Professor of Mathematics, University of Pittsburgh Thomas C. Hales is the Mellon Professor of Mathematics at the University of Pittsburgh. He received B.S. and M.S. degrees from Stanford University, a Tripos Part III from Cambridge University, and a Ph.D. from Princeton University in representation theory under R. P. Langlands. He has held postdoctoral and faculty appointments at MSRI, Harvard University, the University of Chicago, the Institute for Advanced Study, and the University of Michigan. In 1998, Hales, with the help of his graduate student Samuel Ferguson, proved Kepler’s 1611 conjecture (and part of Hilbert’s 18th problem) on the most efficient way to stack oranges. In 2014, he and his coworkers gave a formal proof of the Kepler conjecture in the computer proof assistant “HOL Light.” Hales has received the Chauvenet Prize of the MAA (2003), the Moore Prize (2004), the Robbins Prize of the AMS (2007), the Lester Ford Prize of the MAA (2008), and the Fulkerson Prize of the MPS and AMS (2009). He is an inaugural Fellow of the AMS (2012). His current project is “Formal Abstracts in Mathematics” which will transform mathematical statements from journal articles into a form that can be processed and manipulated by formal proof systems. Participant In: Mechanization of Math Saturday, October 5th, 2019 at 2:30pm Past Event Watch the video » Proof, in the form of step by step deduction, following the rules of logical reasoning, is the ultimate test of validity in mathematics. Some proofs, however, are so long or complex, or both, that they cannot be checked for errors by human experts. In response, a small but growing community of mathematicians, collaborating with computer… read more »
Mechanization of Math Saturday, October 5th, 2019 at 2:30pm Past Event Watch the video » Proof, in the form of step by step deduction, following the rules of logical reasoning, is the ultimate test of validity in mathematics. Some proofs, however, are so long or complex, or both, that they cannot be checked for errors by human experts. In response, a small but growing community of mathematicians, collaborating with computer… read more »