[rck]

Yup! Lean is based on a variant of the Calculus of Constructions, which is in turn based on strong connections between (intuitionistic) natural deduction and type theory. The connection is incredibly beautiful:

https://en.wikipedia.org/wiki/Calculus_of_constructions

[hoping1]

Ah heck, I should have added a section on PTSs, maybe I still will or maybe that will be standalone later. It really is gorgeous stuff!!