BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Lean Meta-theory: The Proofs behind the Proofs - Mario Carneiro (C
 halmers University of Technology)
DTSTART:20250610T104500Z
DTEND:20250610T114500Z
UID:TALK230656@talks.cam.ac.uk
DESCRIPTION:Lean is a theorem prover\, but the theory behind the proof sys
 tem that is implemented is not well understood (by either the users of the
  system or by type theory researchers). In this talk\, I will present some
  recent work on the type theory of lean\, and a progress report on the Lea
 n4Lean project which endeavors to verify a practical lean kernel. I will a
 lso present some novel discoveries regarding the axiomatic strength of Lea
 n's inductive mechanism\, a cornerstone of the theory\, and their implicat
 ions for the development of a tool to automatically check whether proofs i
 n Lean can be replayed to work in ZFC.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR