Date:
Thursday, 14 March, 2024 - 17:00 to 18:00
Speaker:
Professor Adam Topaz (University of Alberta)
Venue:
Live-streamed at MR14 Centre for Mathematical Sciences
Lawvere theories provide a categorical approach to Universal
Algebra, and their models have the benefit of being easily interpreted
in any category with finite products. This talk will discuss a
formalization of (multi-sorted) Lawvere theories in Lean4, as well as
some work in progress toward relating them to the preexisting
algebraic hierarchy.
—-
WATCH ONLINE HERE : https://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting?rtc=1 Meeting ID: 370 771 279 261 Passcode: iCo7a5
Online
Seminar series:
Formalisation of mathematics with interactive theorem provers
