Structures in dependent type theory

Add to your list(s) Download to your calendar using vCal

• Professor Jeremy Avigad (Carnegie Mellon University)
• Thursday 15 February 2024, 17:00-18:00
• Live-streamed at MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Jonas Bayer.

Online

Reasoning about axiomatically characterized abstract structures has been central to mathematics since the early twentieth century. The ability of Lean and its mathematical library, Mathlib, to manage a complex network of such structures has been essential to their acceptance by the mathematical community. In this talk, I will discuss some of the challenges that structural reasoning brings and how they are addressed in Lean and Mathlib. I will also discuss recent work by Joshua Clune, Yicheng Qian, and Alexander Bentkamp toward developing automated reasoning tools that work in such an environment.

—-

WATCH ONLINE HERE : https://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting?rtc=1 Meeting ID: 370 771 279 261 Passcode: iCo7a5

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• Live-streamed at MR14 Centre for Mathematical Sciences
• Online; live-streamed at MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.