LEAN

Lean 4 is a programming language and a tool for both proof assistance and verification that gained traction in the last few years among many mathematicians in different areas of the field. In this SIG, we want to understand how it works, what it can achieve, its limitations and underlying theory, therefore we have initiated a seminar on Lean 4. This seminar is a collaborative and exploratory space for learning Lean 4 and understanding its foundations in Dependent Type Theory. One goal of the seminar is to gain understanding on how to formalize proofs in Lean 4. Beyond this we study the deeper context of Lean 4 by exploring the intersection of dependent type theory, computability theory, proof theory, logic, and category theory.We want to explore both its practical use and its conceptual underpinnings.

More information and a meeting schedule can be found at homepage of the LEAN seminar.