Lean is the dependently typed language with a SotA metaprogramming system. Lean itself is a language written using this system.