What do you mean by "it's logic, mathlib could be implemented in system F"? System F is not dependently typed!
Anyway, nobody doubts that Lean's logic is a dependently typed formalism: "Lean is based on a version of
dependent type theory known as the Calculus of Inductive Constructions" [1]. I thought the discussion here was about using dependent types in programming languages. Note that logics and programming languages are not the same things.
[1] J. Avigad, L. de Moura, S. Kong, Theorem Proving in Lean.
That's an interesting question: can Lean be implemented in Lean's dependent type theory.
I'm not currently working with Lean, but I will start a large verification project in a few months. We have not yet decided which prover to go for. We may write our own.
Anyway, nobody doubts that Lean's logic is a dependently typed formalism: "Lean is based on a version of dependent type theory known as the Calculus of Inductive Constructions" [1]. I thought the discussion here was about using dependent types in programming languages. Note that logics and programming languages are not the same things.
[1] J. Avigad, L. de Moura, S. Kong, Theorem Proving in Lean.