BEGIN:VCALENDAR VERSION:2.0 PRODID:-//CMSA - ECPv6.18.0//NONSGML v1.0//EN CALSCALE:GREGORIAN METHOD:PUBLISH X-ORIGINAL-URL:https://live-hu-cmsa-222.pantheonsite.io X-WR-CALDESC:Events for CMSA REFRESH-INTERVAL;VALUE=DURATION:PT1H X-Robots-Tag:noindex X-PUBLISHED-TTL:PT1H BEGIN:VTIMEZONE TZID:America/New_York BEGIN:DAYLIGHT TZOFFSETFROM:-0500 TZOFFSETTO:-0400 TZNAME:EDT DTSTART:20250309T070000 END:DAYLIGHT BEGIN:STANDARD TZOFFSETFROM:-0400 TZOFFSETTO:-0500 TZNAME:EST DTSTART:20251102T060000 END:STANDARD BEGIN:DAYLIGHT TZOFFSETFROM:-0500 TZOFFSETTO:-0400 TZNAME:EDT DTSTART:20260308T070000 END:DAYLIGHT BEGIN:STANDARD TZOFFSETFROM:-0400 TZOFFSETTO:-0500 TZNAME:EST DTSTART:20261101T060000 END:STANDARD BEGIN:DAYLIGHT TZOFFSETFROM:-0500 TZOFFSETTO:-0400 TZNAME:EDT DTSTART:20270314T070000 END:DAYLIGHT BEGIN:STANDARD TZOFFSETFROM:-0400 TZOFFSETTO:-0500 TZNAME:EST DTSTART:20271107T060000 END:STANDARD END:VTIMEZONE BEGIN:VEVENT DTSTART;TZID=America/New_York:20261014T163000 DTEND;TZID=America/New_York:20261014T173000 DTSTAMP:20261002T183533Z CREATED:20260824T141230Z LAST-MODIFIED:20261002T183533Z UID:10003965-1791995400-1791999000@live-hu-cmsa-222.pantheonsite.io SUMMARY:First Proof Batch 3: Mathematicians putting AI to the test DESCRIPTION:AI for the Working Mathematician \nSpeaker: Lauren Williams\, Harvard \nTitle: First Proof Batch 3: Mathematicians putting AI to the test \nAbstract: First Proof is an initiative that aims to obtain a nuanced\, objective assessment about the capabilities of large language models to prove specified mathematical statements. I will report on the results of First Proof’s third batch of problems. We will be scoring AI-generated solutions based on (1) mathematical correctness\, (2) quality of exposition\, and (3) quality of attributions. URL:https://live-hu-cmsa-222.pantheonsite.io/event/ai_101426/ LOCATION:CMSA Room G10\, CMSA\, 20 Garden Street\, Cambridge\, MA\, 02138\, United States CATEGORIES:AI for the Working Mathematician,Colloquia & Seminar ATTACH;FMTTYPE=image/png:https://live-hu-cmsa-222.pantheonsite.io/media/2026/10/CMSA-AI-for-Mathematicians-Seminar-10.14.2026.docx-scaled.png END:VEVENT BEGIN:VEVENT DTSTART;TZID=America/New_York:20261009T163000 DTEND;TZID=America/New_York:20261009T173000 DTSTAMP:20261002T162101Z CREATED:20260706T172115Z LAST-MODIFIED:20261002T162101Z UID:10003964-1791563400-1791567000@live-hu-cmsa-222.pantheonsite.io SUMMARY:Large Hypercubes DESCRIPTION:AI for the Working Mathematician \nSpeaker: Jordan Ellenberg\, University of Wisconsin-Madison \nTitle: Large Hypercubes \nAbstract: I’ll talk about this paper: Bruhat intervals that are large hypercubes in which we use a tool from Google\, AlphaEvolve\, to discover unexpected combinatorial structures inside the symmetric group (to be precise\, a large hypercube in the Bruhat order.) I’ll talk about why this problem was a good fit for this particular machine learning protocol\, which is a bit different from the most popular prevailing approaches. And I’ll also just talk about this large hypercube\, which is interesting in its own right! URL:https://live-hu-cmsa-222.pantheonsite.io/event/ai_10926/ LOCATION:CMSA Room G10\, CMSA\, 20 Garden Street\, Cambridge\, MA\, 02138\, United States CATEGORIES:AI for the Working Mathematician,Colloquia & Seminar ATTACH;FMTTYPE=image/png:https://live-hu-cmsa-222.pantheonsite.io/media/2026/07/Copy-of-CMSA-AI-for-Mathematicians-Seminar-10.09.2026.docx-scaled.png END:VEVENT BEGIN:VEVENT DTSTART;TZID=America/New_York:20260930T163000 DTEND;TZID=America/New_York:20260930T173000 DTSTAMP:20260924T202814Z CREATED:20260729T160453Z LAST-MODIFIED:20260924T202814Z UID:10003963-1790785800-1790789400@live-hu-cmsa-222.pantheonsite.io SUMMARY:AI for the Working Mathematician DESCRIPTION:AI for the Working Mathematician \nSpeaker: Harold Williams\, USC \nTitle: An Informal Introduction to Formal Proofs \nAbstract: In this talk we will give an introduction to Lean\, a programming language adapted to expressing and verifying proofs. Lean and its flagship library\, mathlib\, have been the focus of a dedicated user community for about a decade\, but their visibility has grown significantly in the last year. This is in large part because Lean makes validating large AI-generated proofs dramatically more practical: the human work is reduced from analyzing the logical correctness of an entire proof to analyzing the semantic correctness of a Lean statement. The main goal of the talk will be to build some example-based intuition for how this works in practice. Time permitting\, we will also discuss how Lean interacts with the way modern AI systems are trained\, and potential implications of formal theorem proving for the broader interaction between science and mathematics. URL:https://live-hu-cmsa-222.pantheonsite.io/event/ai-93026/ LOCATION:CMSA Room G10\, CMSA\, 20 Garden Street\, Cambridge\, MA\, 02138\, United States CATEGORIES:AI for the Working Mathematician,Colloquia & Seminar ATTACH;FMTTYPE=image/png:https://live-hu-cmsa-222.pantheonsite.io/media/2026/07/CMSA-AI-for-Mathematicians-Seminar-9.30.2026.docx-scaled.png END:VEVENT BEGIN:VEVENT DTSTART;TZID=America/New_York:20260923T163000 DTEND;TZID=America/New_York:20260923T173000 DTSTAMP:20260924T151658Z CREATED:20260729T160433Z LAST-MODIFIED:20260924T151658Z UID:10003962-1790181000-1790184600@live-hu-cmsa-222.pantheonsite.io SUMMARY:Finite locally free group schemes DESCRIPTION:AI for the Working Mathematician \nSpeaker: Akhil Mathew\, University of Chicago \nTitle: Finite locally free group schemes \nAbstract: The notion of a finite locally free group scheme is a natural generalization of the usual notion of a finite group. Lagrange’s theorem states that all nth powers vanish in a group of order n. However\, this need not hold for a group scheme. I will explain some history and motivation of this problem and describe a finite locally group scheme of order four (found by AI) where fourth powers are nonzero. \n  URL:https://live-hu-cmsa-222.pantheonsite.io/event/ai_92326/ LOCATION:CMSA Room G10\, CMSA\, 20 Garden Street\, Cambridge\, MA\, 02138\, United States CATEGORIES:AI for the Working Mathematician,Colloquia & Seminar ATTACH;FMTTYPE=image/png:https://live-hu-cmsa-222.pantheonsite.io/media/2026/07/CMSA-AI-for-Mathematicians-Seminar-9.23.2026.docx-1-scaled.png END:VEVENT BEGIN:VEVENT DTSTART;TZID=America/New_York:20260909T163000 DTEND;TZID=America/New_York:20260909T173000 DTSTAMP:20260910T183205Z CREATED:20260706T171637Z LAST-MODIFIED:20260910T183205Z UID:10003960-1788971400-1788975000@live-hu-cmsa-222.pantheonsite.io SUMMARY:Working with LLMs to do high quality math DESCRIPTION:AI for the Working Mathematician \nSpeaker: Daniel Litt\, University of Toronto \nTitle: Working with LLMs to do high quality math \nAbstract: Much hay has been made of the capabilities of LLMs to do math autonomously\, and indeed frontier models have resolved some long-standing\, interesting open questions. But our goal is not to produce papers\, but rather to do high quality mathematics. I’ll discuss some experiments over the past year in trying to get LLMs to help with producing high quality mathematics\, non-autonomously\, and speculate a bit about the future. URL:https://live-hu-cmsa-222.pantheonsite.io/event/ai_9926/ LOCATION:CMSA Room G10\, CMSA\, 20 Garden Street\, Cambridge\, MA\, 02138\, United States CATEGORIES:AI for the Working Mathematician,Colloquia & Seminar ATTACH;FMTTYPE=image/png:https://live-hu-cmsa-222.pantheonsite.io/media/CMSA-AI-for-Mathematicians-Seminar-9.9.2026.docx-scaled.png END:VEVENT END:VCALENDAR