BEGIN:VCALENDAR VERSION:2.0 PRODID:-//132.216.98.100//NONSGML kigkonsult.se iCalcreator 2.20.4// BEGIN:VEVENT UID:20260602T151949EDT-9550JW4a64@132.216.98.100 DTSTAMP:20260602T191949Z DESCRIPTION:Title: Making mathematics computer-checkable\n\nAbstract: In th e last thirty years\, computer proof verification became a mature technolo gy\, with successes including the checking of the Four-Colour Theorem\, th e Odd Order Theorem\, and Hales' proof of the Kepler Conjecture. Recent ad vances such as the 'Liquid Tensor Experiment' verifying a recent theorem o f Scholze have provided further momentum\, as likewise have promising expe riments integrating this technology with machine learning.\n \n I will brief ly describe some of these developments. I will then try to describe\, more generally\, what it *feels* like to carry out research-level computer ver ifications of mathematics proofs: the level of expression one has access t o\, the ways one finds oneself interrogating and reorganizing a paper proo f\, the kinds of arguments which are more tedious (or less tedious!) than on paper.\n\nJoin Zoom Meeting\n https://umontreal.zoom.us/j/85105423917?pw d=enM3MGpFNkZKU2daMjRITmo0N0JUUT09\n Meeting ID: 851 0542 3917\n Passcode: 4 03790\n\nSite web : http://crm.umontreal.ca/colloque-sciences-mathematique s-quebec/index.html#csmq\n DTSTART:20220325T193000Z DTEND:20220325T203000Z SUMMARY:Heather Macbeth (Fordham University) URL:/mathstat/channels/event/heather-macbeth-fordham-u niversity-338547 END:VEVENT END:VCALENDAR