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.

Join Zoom Meeting
Meeting ID: 851 0542 3917
Passcode: 403790

Site web : http://crm.umontreal.ca/colloque-sciences-mathematiques-quebec/index.html#csmq

Follow us on

Back to top