You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Tim Hosgood (Nov 04 2021 at 17:51):starting in 10 minutes (sorry for the late notification!)
https://www.youtube.com/watch?v=Kpa8cCUZLms
Tim Hosgood (Nov 04 2021 at 17:51):Abstract:
Modern logic tells us that mathematics can be formalized, in principle. Computational proof assistants, developed over the last half century, make it possible to do so in practice. In this talk, I will briefly survey the state of the field today and discuss some of the reasons that formalization is desirable. I will discuss one particular proof assistant, Lean, and its library, mathlib. I will explain why dependent type theory, Lean's underlying logical framework, provides an attractive platform for formalization. Finally, I will consider ways that formal mathematics can support and enhance the Topos Institute's missions.