Dependent Type Theory with Lean

Stream: new members

[DSB]

Friends, is there a book or some robust notes on formal Dependent Type Theory (DTT) which uses Lean?
I've been reading the "Theorem Proving in Lean 4", but there is only a small section on DTT.
I've also read the first two chapter of "Type Theory and Formal Proof", but the lack of "code examples" makes the exposition very dry.

[Kevin Buzzard]

Is https://browncs1951x.github.io/static/files/hitchhikersguide.pdf to your taste?

[DSB]

Thanks! This looks very good.

[Vlad Tsyrklevich]

DSB said:

I've also read the first two chapter of "Type Theory and Formal Proof", but the lack of "code examples" makes the exposition very dry.

If you find the hitchhikers guide assumes too much prior knowledge, Type Theory and Formal Proof gets to explaining dependent types/the calculus of constructions half-way through the book, and then the rest of the book is putting the first half to work to prove a particular theorem from the ground-up.