[pl-seminar] Fwd: Tom Hales Distinguished Lectures

[Thomas Reps <reps@xxxxxxxxxxx>]

Please note that on November 3,4,5 (Weds, Thurs, Fri) Tom Hales will
give this semester's distinguished lectures at 4pm in B239 VV. He will
give an extra lecture (the 4th one below) as a number theory seminar
at 2:30pm on Nov 4 in B105 VV.

The talks will all be aimed at a general mathematical audience and
will be largely independent of one another.


1.  Title: Introduction to Formal Proofs.

Abstract:  In a formal proof, every step of a proof is checked, all the
way back to the fundamental axioms and rules of inference of mathematics.
A formal proof is often less intuitive than an ordinary proof, but it is
also less prone to errors.  In recent years, a number of nontrivial theorems
have been checked formally, including the proof of the four-color theorem,
two different proofs of the prime number theorem, Cauchy's theorem,
and three different proofs of the Jordan curve theorem.  This talk
will give a general introduction to formal proofs and will
describe some of these formal proofs.

2.  Title: Towards a Formal Proof of Kepler conjecture on Sphere Packings.

Abstract: The Kepler Conjecture asserts that the densest packing of
congruent balls in three dimensional Euclidean space is obtained by
placing them in the familiar pyramid arrangement, used to arrange
oranges at the fruit stand and to arrange cannonballs at war
memorials.  This problem was solved in 1998 by Sam Ferguson and me.
The solution is about 300 pages long and relies on long computer
calculations.  I am now involved in a long-term collaborative project
to give a formal proof of the Kepler conjecture. This project was
original estimated to require 20-research years to complete.  Now,
after several years and three Ph.D. dissertations the project is
nearing completion.  This talk will describe how to transcribe a
difficult mathematical proof such as the sphere packing problem into a
formal proof system and will point out what remains to be done to
complete the project.

3.  Title: Proof Assistants in Practice.

Abstract: A proof assistant is a piece of computer software that
checks the logical steps in a mathematical proof.  This talk will
describe the design of a particular proof assistant called "HOL
Light."  It will give a basic tutorial about how to install and use
HOL Light.  It will demonstrate the construction of some simple
mathematical proofs inside this system.

*****************************************************************************
Number theory seminar:

4.  Title: Fundamental Lemma for beginners.

Abstract: At the International Congress of Mathematicians in India in
August, Ngo Bao Chau was awarded a Fields medal for his proof of the
"Fundamental Lemma."  This talk is particularly intended for students
and mathematicians who are not specialists in the theory of
Automorphic Representions.  I will describe the significance and some
of the applications of the "Fundamental Lemma."  I will explain why
this problem turned out to be so difficult to solve and will give some
of the key ideas that go into the proof.




Short Bio: 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, completed Tripos Part III at Cambridge
University, and received Ph.D. from Princeton University under
Langlands in representation theory. 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 a graduate student Samuel
Ferguson, proved Kepler?s 1611 conjecture (and part of Hilbert?s 18th
problem) on the most efficient way to stack oranges. Hales?s current
project, called Flyspeck, seeks to formalize his proof of the Kepler
conjecture in the computer proof assistant ?HOL Light.?


----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.