BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//CMSA - ECPv6.15.17//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: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
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20230312T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20231105T060000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/New_York:20220914T120000
DTEND;TZID=America/New_York:20220914T130000
DTSTAMP:20260404T214155
CREATED:20240214T114614Z
LAST-MODIFIED:20240229T110925Z
UID:10002707-1663156800-1663160400@cmsa.fas.harvard.edu
SUMMARY:Strategyproof-Exposing Mechanisms Descriptions
DESCRIPTION:Colloquium \nSpeaker: Yannai Gonczarowski (Harvard)\n\nTitle: Strategyproof-Exposing Mechanisms Descriptions \nAbstract: One of the crowning achievements of the field of Mechanism Design has been the design and usage of the so-called “Deferred Acceptance” matching algorithm. Designed in 1962 and awarded the Nobel Prize in 2012\, this algorithm has been used around the world in settings ranging from matching students to schools to matching medical doctors to residencies. A hallmark of this algorithm is that unlike many other matching algorithms\, it is “strategy-proof”: participants can never gain by misreporting their preferences (say\, over schools) to the algorithm. Alas\, this property is far from apparent from the algorithm description. Its mathematical proof is so delicate and complex\, that (for example) school districts in which it is implemented do not even attempt to explain to students and parents why this property holds\, but rather resort to an appeal to authority: Nobel laureates have proven this property\, so one should listen to them. Unsurprisingly perhaps\, there is a growing body of evidence that participants in Deferred Acceptance attempt (unsuccessfully) to “game it\,” which results in a suboptimal match for themselves and for others. \nBy developing a novel framework of algorithm description simplicity—grounded at the intersection between Economics and Computer Science—we present a novel\, starkly different\, yet equivalent\, description for the Deferred Acceptance algorithm\, which\, in a precise sense\, makes its strategyproofness far more apparent. Our description does have a downside\, though: some other of its most fundamental properties—for instance\, that no school exceeds its capacity—are far less apparent than from all traditional descriptions of the algorithm. Using the theoretical framework that we develop\, we mathematically address the question of whether and to what extent this downside is unavoidable\, providing a possible explanation for why our description of the algorithm has eluded discovery for over half a century. Indeed\, it seems that in the design of all traditional descriptions of the algorithm\, it was taken for granted that properties such as no capacity getting exceeded should be apparent. Our description emphasizes the property that is important for participants to correctly interact with the algorithm\, at the expense of properties that are mostly of interest to policy makers\, and thus has the potential of vastly improving access to opportunity for many populations. Our theory provides a principled way of recasting algorithm descriptions in a way that makes certain properties of interest easier to explain and grasp\, which we also support with behavioral experiments in the lab. \nJoint work with Ori Heffetz and Clayton Thomas.
URL:https://cmsa.fas.harvard.edu/event/collquium-title-tba/
LOCATION:CMSA Room G10\, CMSA\, 20 Garden Street\, Cambridge\, MA\, 02138\, United States
CATEGORIES:Colloquium
ATTACH;FMTTYPE=image/png:https://cmsa.fas.harvard.edu/media/CMSA-Colloquium-09.14.22-1.png
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=America/New_York:20220914T140000
DTEND;TZID=America/New_York:20220914T150000
DTSTAMP:20260404T214155
CREATED:20230808T183823Z
LAST-MODIFIED:20240301T091205Z
UID:10001210-1663164000-1663167600@cmsa.fas.harvard.edu
SUMMARY:Breaking the one-mind-barrier in mathematics using formal verification
DESCRIPTION:New Technologies in Mathematics Seminar \nSpeaker: Johan Commelin\, Mathematisches Institut\, Albert-Ludwigs-Universität Freiburg \nTitle: Breaking the one-mind-barrier in mathematics using formal verification \nAbstract: In this talk I will argue that formal verification helps break the one-mind-barrier in mathematics. Indeed\, formal verification allows a team of mathematicians to collaborate on a project\, without one person understanding all parts of the project. At the same time\, it also allows a mathematician to rapidly free mental RAM in order to work on a different component of a project. It thus also expands the one-mind-barrier. \nI will use the Liquid Tensor Experiment as an example\, to illustrate the above two points. This project recently finished the formalization of the main theorem of liquid vector spaces\, following up on a challenge by Peter Scholze. \nVideo
URL:https://cmsa.fas.harvard.edu/event/breaking-the-one-mind-barrier-in-mathematics-using-formal-verification/
LOCATION:CMSA Room G10\, CMSA\, 20 Garden Street\, Cambridge\, MA\, 02138\, United States
CATEGORIES:New Technologies in Mathematics Seminar
END:VEVENT
END:VCALENDAR