|
A formal proof is a proof in which every logical inference has
been checked all the way back to the fundamental axioms of mathematics. The number of primitive inferences can run
into the millions, even for a traditional proof of modest size. A number of noteworthy theorems have now
been checked formally, including the four-color theorem, the Jordan curve
theorem, and the prime number theorem (both the elementary and analytic
proofs). This talk will describe the current
stage of development of formal theorem proving technology. It will describe some research projects
aimed at bringing formal theorem proving to every mathematician's desktop.
Brief
CV
*Thomas Hales is Mellon
Professor of Mathematics at the University
of Pittsburgh. He
received his PhD from Princeton University under the supervision of Robert Langlands, and has held positions at MSRI Berkeley, Harvard
University, University
of Chicago and University
of Michigan as well as membership at
the Institute for Advanced Study, Princeton.
He is best known for his (computer-aided) proof of the Kepler's
conjecture, one of the oldest problems in discrete geometry, as well as the
honeycomb conjecture. Hales advocates the formalization of mathematics to
ensure rigor in an era where proofs are becoming increasingly complex and
computers are becoming necessary to perform verification. He has received
many prizes and honors for his work, including the Chauvenet
Prize (2003), the R. E. Moore Prize (2004) the Robbins Prize (2007), the
Lester Ford Prize (2008) and the Fulkerson Prize (2009). Hales has been
invited to speak at many international meetings and conferences, including
the Institute for Advanced Study, Public lecture series (1999), the National
Academy of Science, Frontiers of Science Symposium (1999), the Joint
Mathematical Meetings, AMS-MAA-SIAM (2000), the Euler Lecture at Berlin
(2000), the International Congress of Mathematicians (2002), the Institute
for Math and its Applications (IMA), Public Lecture Series (2005), the
Institute for the Mathematical Sciences (PIMS) Distinguished Chair lectures
(2006) and the Arnold Ross Lecture of the AMS (scheduled October 2010).
|