reading suggestion to what dependent type theory is?

Stream: new members

[rzeta0]

I've reached the point in my learning now where I can't put off knowing at the surface level what "dependent type theory" is.

Can anyone suggest a short beginner-friendly (min jargon) overview?

My aim is to understand (not in detail) how Lean uses it to validate proofs.

For example - I have a rough idea how Prolog uses a "search" to answer logic queries against a database of propositions.

I read somewhere that most previous theorem proof checkers used "set theory" but Lean took a different approach - but I have no clue how you would do it differently to axiomatic set theory.

If I had to guess I would say that Lean/mathlib uses the idea that everything is a "type" and the rigour of this means that it can reason about them, using inference from built-in facts and also facts provides by the user's proof, augmented by helpful rules in mathlib.

[Mario Carneiro]

You could try #tpil or the axioms section of the new lean reference manual

[Mario Carneiro]

BTW it's not true that most previous proof checkers used set theory, set theory based proof assistants are in the minority.

• Set theory: Metamath, Mizar
• Simple type theory: HOL4, HOL Light, Isabelle, ProofPower, PVS
• Dependent type theory: Automath, Lean, Coq, Agda

[rzeta0]

thanks I'll try the chapter 2 in TPIL

[Julian Berman]

Perhaps it's also worth double checking that you really mean to specifically learn about dependent type theory, and not that you're trying to learn a bit more about the Curry-Howard correspondence.

[Julian Berman]

(Either way possibly the resource is the same.)

[rzeta0]

@Julian Berman - good question. I started typing an answer but realised I can't really add more than "I just want to know roughly how it works internally - what the big idea is".

Perhaps I'll be able to know better what I want to know once I've read chapter 3 of TPIL.