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:20261014T140000
DTEND;TZID=America/New_York:20261014T150000
DTSTAMP:20260929T165604Z
CREATED:20260729T193937Z
LAST-MODIFIED:20260929T165604Z
UID:10004013-1791986400-1791990000@live-hu-cmsa-222.pantheonsite.io
SUMMARY:Prove2Me: Formalizing Fermat Last Theorem and Beyond
DESCRIPTION:New Technologies in Mathematics Seminar \nSpeaker: Tianyi Peng\, Decision\, Risk\, and Operations Division\, Columbia Business School \nTitle: Prove2Me: Formalizing Fermat Last Theorem and Beyond \nAbstract: Proof assistants such as Lean 4 promise the paradigm of formally verified mathematics\, but large-scale formalization projects have faced major barriers to entry\, including the need for expertise in formal verification (as well as the underlying mathematics) and the significant time required for writing formal proofs. AI coding agents have dramatically reduced these barriers; human users can now use natural language to prompt agents to write complex proofs in Lean. This opens up the intriguing possibility of internet-scale mathematical collaboration involving both humans and AI agents\, where correctness is machine-checked.
URL:https://live-hu-cmsa-222.pantheonsite.io/event/newtech_101426/
LOCATION:Virtual
CATEGORIES:New Technologies in Mathematics Seminar
ATTACH;FMTTYPE=image/png:https://live-hu-cmsa-222.pantheonsite.io/media/2026/07/CMSA-NTM-Seminar-10.14.2026.docx-scaled.png
END:VEVENT
END:VCALENDAR