Logic Seminar

The Logic Seminar is a joint LOS/IMAR/ILDS seminar, featuring talks on mathematical logic, philosophical logic and logical aspects of computer science.

All seminars, except where otherwise indicated, will be on Thursdays between 14:00 and 16:00, Bucharest time. The seminars are held locally at Hall 203 of the Faculty of Mathematics and Computer Science, University of Bucharest (in the new PBTower location), but can also be occasionally held remotely.

To receive announcements about the seminar, please send an email to logic-seminar@ilds.ro.

Organizers: Laurențiu Leuștean, Andrei Sipoș

Past Talks in 2025-2026

Thursday, May 28, 2026

Horațiu Cheval (University of Bucharest)

An introduction to the type theory of Lean

Abstract:

In this talk, we present an overview of the type theory on which the Lean theorem prover is based, which is a version of the Calculus of Inductive Constructions, with definitional proof irrelevance, quotient types, propositional extensionality, and the axiom of choice.We begin with an introduction to dependent types, focusing on the particular flavor present in Lean, noting its distinguishing features and how they reflect in the practical use of the prover.

We will then go over some of the metatheoretical properties of the system, such as its equiconsistency with ZFC +{there exist n inaccessible cardinals | n < ω}, undecidability of definitional equality, and failure of normalization.

The presentation will largely follow [1], which describes Lean 3, but we will also explain the few changes that occurred in Lean 4, the current version.

References:

[1] Mario Carneiro, The Type Theory of Lean, Master’s thesis, Carnegie Mellon University, 2019. 

Past Seminars