The Type Theory of Lean 4

Stream: lean4

[Rafael Oliveira Cavalcante]

Is there a version of the paper “The Type Theory of Lean” (Mario Carneiro) for Lean 4? I also would like to know if there’s graph showing the dependency of each component of mathlib or mathlib4. Besides, that paper show the construction of Lean in ZFC. Is there a paper that shows the opposite (ZFC in Lean)? Thank you for your attention!

[Yaël Dillies]

For the reverse, there's better than a paper. There's the actual construction! See file#set_theory/zfc/basic (it's not yet ported to Lean 4).

[Ruben Van de Velde]

ZFC in lean3 is https://leanprover-community.github.io/mathlib_docs/set_theory/zfc/basic.html , I think

[Horațiu Cheval]

As for the theory of Lean 4 vs Lean 3, I had the same question some time ago, answered here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Type.20theory.20of.20lean.204

[Mario Carneiro]

My understanding is that @Sebastian Ullrich 's thesis contains a part which extends the results of my thesis to lean 4. I don't know whether it is publicly available though

[Sebastian Ullrich]

It is not available yet, no

[Ruben Van de Velde]

Ruben Van de Velde said:

ZFC in lean3 is https://leanprover-community.github.io/mathlib_docs/set_theory/zfc/basic.html , I think

And it's ported to lean 4 now as well