LEAN

The SIG aims at understanding LEAN, its foundations in dependent type theory, and practical use cases. Specific goals are

• learning how to formalize proofs in LEAN, and
• exploring the intersection of dependent type theory, computability theory, proof theory, logic, and category theory.

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