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 (Aug 09 2021 at 10:24):Abstract:
Lean is a computer proof checker developed by Microsoft Research. Over the last four years I have been part of a team of mathematicians and computer scientists who have got it into their heads that it is somehow "obviously" a good idea to build a formally verified library of modern mathematics in Lean. You can think of it as a 21st century Bourbaki if you like, although our plans are actually far grander than Bourbaki's. I will talk about two things: (1) how it's going and (2) why we're doing it. No background in computer proof checkers will be necessary to follow the talk.
Zoom: https://topos-institute.zoom.us/j/5344862882?pwd=Znh3UlUrek41T3RLQXJVRVNkM3Ewdz09
YouTube: https://youtu.be/alByz_LoANE
Henry Story (Aug 09 2021 at 11:50):Note: Kevin Buzzard's talk will take place on 12th of August, 2021.
Tim Hosgood (Aug 09 2021 at 19:56):oh yes, sorry, i forgot to mention that key point, thank you!
Tim Hosgood (Aug 09 2021 at 19:56):17:00UTC as per usual