BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//CMSA - ECPv6.17.5.1//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-ORIGINAL-URL:https://cmsa.fas.harvard.edu
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:20260930T163000
DTEND;TZID=America/New_York:20260930T173000
DTSTAMP:20260924T202814Z
CREATED:20260729T160453Z
LAST-MODIFIED:20260924T202814Z
UID:10003963-1790785800-1790789400@cmsa.fas.harvard.edu
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://cmsa.fas.harvard.edu/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://cmsa.fas.harvard.edu/media/2026/07/CMSA-AI-for-Mathematicians-Seminar-9.30.2026.docx-scaled.png
END:VEVENT
END:VCALENDAR