I am interested in learning LEAN. Visiting some forums and archives it seems that this uses type theory. Specifically, the "calculus of inductive constructions" is mentioned.
I have general knowledge in logic, but I'm not sure this is enough. I am interested in knowing how much knowledge I must have in lambda calculus and type theory, to move on to the study of calculus of inductive constructions, or more precisely, to start writing code. In the same way, if you could provide me with a bibliography to accelerate learning, I would greatly appreciate it.
The Lean Theorem Prover Github site (https://leanprover.github.io/) is the best resource from a practitioner's perspective. If you intend to write Lean code then this is probably the fastest route.
The same site also has an extensive list of publications at https://leanprover.github.io/publications/ that you may be interested in, if you want to understand the theoretical underpinnings of Lean.