[jojo3000]

Lean is LCF style in the sense that there is a small kernel, and all proofs written by the user and generated by the automation are checked by this kernel. This kernel (i.e. type checker) is much smaller than that of Coq or Agda.

It is _not_ LCF style in the sense that there is only a "theorem" datatype with proof operations. Lean proofs are type-checked expressions.

It is hard to find a terse description of the Calculus of Constructions or CIC. Lean's logic essentially consists of Martin-Löf type theory + (noncumulative) universes with Impredicative Prop + inductive type (where nested and mutual induction is compiled down to a simpler forms with only one eliminator) + quotient types + function and Prop extensionality. And optionally choice to gain a classical logic. Most other features, like a Agda like dependent pattern matching, or mutual and nested inductive types are compiled down to more basic features.

[xgk]

    there is only a "theorem" datatype 

You mean that there is NOT only a "theorem" datatype? In contrast to Curry/Howard provers, the LCF approach forgets proofs, it guarantees soundness by giving you access to proof rules only through the "theorem" datatype (which is the key trusted computing base). To be sure the "theorem" datatype may internally maintain a proof object (e.g. for the purposes of program extraction), but that's not necessary.

[jojo3000]

Sorry, I was unclear. I meant that most LCF style theorem provers only have one theorem datatype to carry proof information.