1. Etusivu
  2. Ajankohtaista
  3. SMY:n Etäkollokvio Ke 18.10.

SMY:n etäkollokvio ke 18.10.

Making mathematics computer-checkable

Recording on YouTube: https://youtu.be/YbntYOs8gUQ

 

Time and place: Wednesday, October 18 at 16:15, over Zoom and in colloquium watch events at mathematics departments (see bottom of the page)

Speaker: Heather Macbeth (Fordham University)

Title: Making mathematics computer-checkable

Abstract: 

In the last thirty years, computer proof verification became a mature technology, with successes including the checking of the Four-Colour Theorem, the Odd Order Theorem, and Hales' proof of the Kepler Conjecture. Recent advances such as the "Liquid Tensor Experiment" verifying a recent theorem of Scholze have provided further momentum, as likewise have promising experiments integrating this technology with machine learning.

I will briefly describe some of these developments. I will then try to describe, more generally, what it feels like to carry out research-level computer verifications of mathematics proofs: the level of expression one has access to, the ways one finds oneself interrogating and reorganizing a paper proof, the kinds of arguments which are more tedious (or less tedious!) than on paper. 

Image
Heather Macbeth [image from https://faculty.fordham.edu/hmacbeth1/ used with permission]
The speaker, Heather Macbeth, is an assistant professor at Fordham University, with research interests in Kähler geometry and in geometric analysis. She obtained a PhD in 2015 at Princeton University under the supervision of Gang Tian, and she was a C. L. E. Moore Instructor at MIT and a postdoctoral researcher at ENS. She is one of the maintainers of Lean's mathematical library Mathlib.

 

Where to watch?

The colloquium will be broadcast over Zoom on Wednesday, October 18, at 16:15.

In addition there will be colloquium watch events at most Finnish universities' mathematics departments. See the list below for the location of your own department's event:

  • Aalto University: lecture hall M1 (Otakaari 1)
  • Tampere University: Pinni B0020 (keskustakampus)
  • University of Helsinki: lecture hall Exactum B123
  • University of Jyväskylä: hall MaD302
  • University of Oulu: lecture theatre L9
  • University of Turku: seminar room M3 (Quantum)
  • University of Vaasa: F487 (Tyynen tupa)
  • Åbo Akademi: Aurum A316 Chromium (Henrikinkatu 2)

Recording on YouTube: https://youtu.be/YbntYOs8gUQ