University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Prospects for formalizing the theory of weak infinite-dimensional categories

  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

Prospects for formalizing the theory of weak infinite-dimensional categories

Download to your calendar using vCal

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

A peculiarity of the ∞-categories literature is that proofs are often written without reference to a concrete definition of an ∞-category, a practice that creates an impediment to formalization. We describe three broad strategies that would make ∞-category theory formalizable, which may be described as “analytic,” “axiomatic,” and “synthetic.” We then highlight two parallel ongoing collaborative efforts to formalize ∞-category theory in two different proof assistants: the “axiomatic” theory in Lean and the “synthetic” theory in Rzk. We show some sample formalized proofs to highlight the advantages and drawbacks of each approach and explain how you could contribute to this effort. This involves joint work with Mario Carneiro, Nikolai Kudasov, Dominic Verity, Jonathan Weinberger, and many others.

=== Online talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1

Meeting ID: 871 4336 5195

Passcode: 541180

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

Room 12, History Faculty Gates Scholars Common Room, University Centre on Mill Lane CMS, Room to be confirmed

Other talks

TBC Shining a light on the origin of supermassive black holes with cosmological simulations Title to be confirmed Favourite Plants: the common, the captivating, and the curious Market Failure, Organ Shortage, Pandemic and Climate Change: The Architecture of Cooperation Zooming in on the assembly of galaxies in the early Universe
 

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