Documentation of Lean's architecture

Stream: new members

[Horatiu Cheval]

I've seen people discussing various components such as the kernel, the VM or the elaborator, but I don't have a clear picture of what everything does and how it fits together. Is there a place where I can learn about these things?

[Bryan Gin-ge Chen]

I don't know that there's a single good place to read about this, but there are a bunch of papers and presentations on the official Lean website. The more detailed papers "The Lean Theorem Prover" and "Elaboration in Dependent Type Theory" are quite out-of-date since they describe Lean 2 but might still be helpful.

[Horatiu Cheval]

Thanks, I checked the papers, they explained pretty much what I wanted to know. I suppose the general notions carry over from Lean 2 to the newer versions.