University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Structures in dependent type theory

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Structures in dependent type theory

Download to your calendar using vCal

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:

Note that ex-directory lists are not shown.

Other lists

Mp3 Music Download Purple Gemstones Average on weekdays: 9200.87153652 kWh

Other talks

Packing the Border: Quail Crates and the Regulation of Animal Movement on the US-Mexico Border, 1910s-1940s Morning Break Loke CTR Annual Meeting 2026 - Epigenetics of embryogenesis and placentation Polar Oceans Seminar Talk Novel neuroimaging methods in Lewy body dementia Title to be confirmed
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity