What's the formal type system of Lean?

Stream: Berkeley Lean Seminar

[Kentarô YAMAMOTO]

What's a good reference about the formal type system of Lean in the form of "it is the usual inference rules of CIC plus such and such additional rules/axioms"? I would like to see all of the actual formal rules/axioms in one place instead of a textbook-like walkthough.

[Kevin Buzzard]

Mario Carneiro's MSc thesis

[Patrick Lutz]

Link: https://github.com/digama0/lean-type-theory/releases/tag/v1.0

[Kentarô YAMAMOTO]

Thank you, Patrick!