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:20210407T150000
DTEND;TZID=America/New_York:20210407T160000
DTSTAMP:20240515T193258Z
CREATED:20240126T073259Z
LAST-MODIFIED:20240515T193258Z
UID:10001398-1617807600-1617811200@cmsa.fas.harvard.edu
SUMMARY:Type theory from the perspective of artificial intelligence
DESCRIPTION:Speaker: David McAllester – Toyota Technological Institute at Chicago \nTitle: Type theory from the perspective of artificial intelligence \nAbstract: This talk will discuss dependent type theory from the perspective of artificial intelligence and cognitive science. From an artificial intelligence perspective it will be argued that type theory is central to defining the “game” of mathematics — an action space and reward structure for pure mathematics. From a cognitive science perspective type theory provides a model of the grammar of the colloquial (natural) language of mathematics. Of particular interest is the notion of a signature-axiom structure class and the three fundamental notions of equality in mathematics — set-theoretic equality between structure elements\, isomorphism between structures\, and Birkoff and Rota’s notion of cryptomorphism between structure classes. This talk will present a version of type theory based on set-theoretic semantics and the 1930’s notion of structure and isomorphism given by the Bourbaki group of mathematicians. It will be argued that this “Bourbaki type theory” (BTT) is more natural and accessible to classically trained mathematicians than Martin-Löf type theory (MLTT). BTT avoids the Curry-Howard isomorphism and axiom J of MLTT. The talk will also discuss BTT as a model of MLTT. The BTT model is similar to the groupoid model in that propositional equality is interpreted as isomorphism but different in various details. The talk will also briefly mention initial thoughts in defining an action space and reward structure for a game of mathematics.
URL:https://cmsa.fas.harvard.edu/event/4-7-2021-new-technologies-in-mathematics-seminar/
CATEGORIES:New Technologies in Mathematics Seminar
ATTACH;FMTTYPE=image/png:https://cmsa.fas.harvard.edu/media/CMSA-New-Technologies-in-Mathematics-04.07.21.png
END:VEVENT
END:VCALENDAR