Lean is a theorem prover, but the theory behind the proof system 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 Lean4Lean project which endeavors to verify a practical lean kernel. I will also present some novel discoveries regarding the axiomatic strength of Lean's inductive mechanism, a cornerstone of the theory, and their implications for the development of a tool to automatically check whether proofs in Lean can be replayed to work in ZFC.
