skip to content

Department of Computer Science and Technology

Thursday, 14 March, 2024 - 17:00 to 18:00
Professor Adam Topaz (University of Alberta)
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 : Meeting ID: 370 771 279 261 Passcode: iCo7a5

Seminar series: 
Formalisation of mathematics with interactive theorem provers

Upcoming seminars