Essén lectures
These lectures are presented by eminent experts and are aimed at a general audience of PhD students. Doctoral students who pass the assignments will receive 3 credits. The lecture series is named after Professor Matts Essén (1932-2003), who worked at Uppsala University until his retirement in 1997.
Essén Lectures 2024:
10-14 June, Heather Macbeth (Fordham)
"Computer formalization and a theorem about Gromov hyperbolicity"
In the last ten years, formalization – building up proofs as line-by-line logical deductions from the axioms of mathematics, with the help of specialized computer systems – has seen increasing interest from mathematicians. Two of the main points of appeal of formalization are (1) a guarantee of correctness, including in technical arguments where mathematicians tend to lose their intuition; (2) an interactive work environment in which different approaches can be experimented with without the risk of introducing inconsistencies.
I will lecture on a theorem whose formalization illustrates both these advantages. In geometric group theory, the proof of the robustness of the "hyperbolic group" concept depends on the so-called Morse lemma for (Gromov-)hyperbolic metric spaces. Shchur (2013) gave a "quantitative" version of this Morse lemma, optimal (up to a constant) in its dependence on the geometric quantities in the configuration considered. Gouëzel tried to formalize this proof in Isabelle and discovered an error. In joint work in 2018, simultaneously formalized, they gave a correct proof, and, exploiting the formalization for ease of experimentation, dramatically improved the constant.
My lectures will alternate between the presentation of (a simplified version of) the Gouëzel-Shchur theorem and an introduction to formalization. I will specifically concentrate on the skills of reading and modifying an existing formalization, since these can be learned more quickly than the skill of formalizing a theory from scratch. Later in the week, student projects will explore some of the improvements to the constant in the theorem, using the formalization as an essential tool.
The schedule each day is planned as follows:
Monday 10/6
12:00-13:15 Lunch
13:15-14:00 Lecture 1 in Å4001
14:15-15:00 Lecture 2 in Å4001
14:15-15:00 Data lab in Å4002 (bring your own Laptop)
Tuesday 11/6
12:30-14:15 Lunch
14:15-15:00 Lecture 1 in Å4001
15:15-16:00 Lecture 2 in Å4001
16:15-17:00 Data lab in Å4002 (bring your own Laptop)
Wednesday 12/6
10:15-11:00 Lecture 1 in i Å4001
11:15-12:00 Lecture 2 in Å4001
12:00-14:15 Lunch
13:15-14:00 Data lab in Å4002 (bring your own Laptop)
Thursday 13/6
10:15-11:00 Lecture 1 in i Å4001
11:15-12:00 Lecture 2 in Å4001
12:00-14:15 Lunch
13:15-15:00 Data lab in Å4002 (bring your own Laptop)
18:00 Conference dinner at China! (Kungsängsgatan 20)
Friday 14/6
10:15-11:00 Lecture 1 in i Å4001
11:15-12:00 Lecture 2 in Å4001
12:00-14:15 Lunch
Previous Essén Lectures:
2023 Tuomas Hytönen (Helsingfors) Weighted extrapolation, old and new
2020-2022 Inga Essén-föreläsningar på grund av covid-19
2019 Hubert Bray (Duke) Geometry, Black Holes, and Dark Matter: An Introduction
2018 Ioannis Karatzas (Columbia) Stochastic finance
2017 Jacob Rasmussen (Cambridge) Knot polynomials and knot homologies
2016 Christian Krattenthaler (Wien) The art of bijection
2015 Wilhelm Schlag (Chicago) An introduction to nonlinear wave equation
2014 Francois Baccelli (Austin) Stochastic geometry
2013 Alexander Kleshchev (Oregon) The symmetric group: its combinatorics, representations and applications
2012 Jens Marklof (Bristol) Emerging applications of homogeneous dynamics: From discrete mathematics to statistical physics