Upcoming Events

Alfred Tarski Lectures

April 22, 2019, 4:00 PM (4 LeConte Hall)

Thomas Hales
Andrew Mellon Professor of Mathematics, University of Pittsburgh

A formal proof of the Kepler conjecture

The Kepler Conjecture asserts that no packing of congruent balls in three-dimensional Euclidean space can have density greater than that of the face-centered cubic packing. This talk will describe the history and proof of the conjecture, including early attempts to reduce the problem to a finite calculation, controversy surrounding claimed proofs, the announcement of a proof by Sam Ferguson and me more than 20 years ago, and finally a formal proof of the Kepler conjecture in the HOL Light proof assistant in 2014.

Alfred Tarski Lectures

April 24, 2019, 4:00 PM (4 LeConte Hall)

Thomas Hales
Andrew Mellon Professor of Mathematics, University of Pittsburgh

Formalizing mathematics

This talk will describe a broad long-term research program to make formal proofs in mathematics a practical reality. A formal proof is a mathematical proof that has been checked exhaustively by computer, on the basis of the fundamental axioms of mathematics and the primitive inference rules of logic. The field has progressed to the point that it is now possible to give formal proofs of major theorems in mathematics.

Alfred Tarski Lectures

April 26, 2019, 4:00 PM (60 Evans Hall)

Thomas Hales
Andrew Mellon Professor of Mathematics, University of Pittsburgh

Integrating with Logic

In 1995, Kontsevich introduced a new form of integration, call motivic integration. From the start, the development of motivic integration has been guided by model theory, especially quantifier elimination. One particularly useful result has been a far-reaching generalization of the Ax-Kochen-Ersov transfer principle in logic to integration. This talk will give a gentle introduction to motivic integration and will highlight some applications to the Langlands program.