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.
![Heather Macbeth [image from https://faculty.fordham.edu/hmacbeth1/ used with permission]](/sites/matemaattinenyhdistys.fi/files/2023-10/heather_macbeth.jpeg)
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