# The Alfred Tarski Lectures

Following the death of Group founder Alfred Tarski in 1983, an endowment fund was established in his memory. Using income from this fund, a series of annual Alfred Tarski Lectures was inaugurated in 1989. Each spring an outstanding scholar in a field to which Tarski contributed is selected to come to Berkeley to meet with faculty and students and to deliver several lectures. (List of past Tarski lectures.)

## The Thirty-first Annual Alfred Tarski Lectures

**Thomas Hales**

Andrew Mellon Professor of Mathematics, University of Pittsburgh

*A formal proof of the Kepler conjecture*

Monday, April 22, 2019

4 PM, 4 LeConte HallThe 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.

*Formalizing mathematics*

Wednesday, April 24, 2019

4 PM, 4 LeConte HallThis 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.

*Integrating with Logic*

Friday, April 26, 2019

4 PM, 60 Evans HallIn 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.