BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//CMSA - ECPv6.17.1//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:CMSA
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:20200308T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20201101T060000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20210314T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20211107T060000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20220313T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20221106T060000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/New_York:20210113T150000
DTEND;TZID=America/New_York:20210113T160000
DTSTAMP:20240517T201031Z
CREATED:20240126T093843Z
LAST-MODIFIED:20240517T201031Z
UID:10001441-1610550000-1610553600@cmsa.fas.harvard.edu
SUMMARY:AI and Theorem Proving
DESCRIPTION:Speaker: Josef Urban\, Czech Technical University \nTitle: AI and Theorem Proving \nAbstract: The talk will discuss the main approaches that combine machine learning with automated theorem proving and automated formalization. This includes learning to choose relevant facts for “hammer” systems\, guiding the proof search of tableaux and superposition automated provers by interleaving learning and proving (reinforcement learning) over large ITP libraries\, guiding the application of tactics in interactive tactical systems\, and various forms of lemmatization and conjecturing. I will also show some demos of the systems\, and discuss autoformalization approaches such as learning probabilistic grammars from aligned informal/formal corpora\, combining them with semantic pruning\, and using neural methods to learn direct translation from Latex to formal mathematics.
URL:https://cmsa.fas.harvard.edu/event/1-13-2021-new-technologies-in-mathematics/
LOCATION:Virtual
CATEGORIES:New Technologies in Mathematics Seminar
ATTACH;FMTTYPE=image/png:https://cmsa.fas.harvard.edu/media/CMSA-New-Technologies-in-Mathematics-01.13.21.png
END:VEVENT
END:VCALENDAR