I'm aware of Lean's type theory. Did the type theory of lean change at all as we moved to Lean 4? Are there any references to this?
Some things changed but the type theory stayed exactly the same, so e.g. https://github.com/digama0/lean-type-theory/releases/tag/v1.0 is still a valid reference (edit: apparently this is not completely correct -- see Sebastian's comment below)
As already commented by Sebastian Ullrich, there are a few small changes to the Lean 4 kernel, detailed in his PhD thesis. Now, that it is done (and has been for a few months), I want to make sure it gets the attention it deserves. The details on the kernel are in Section 3.2.