The primary culture around Lean is mathematicians looking to prove mathematics. AFAICT Lean is just about the right power for that.

Agda, OTOH, is IMO the dependently typed language for type theorists, and does weird things, but "unproductive" is applicable only for a somewhat narrow view of productivity.

I don't consider there to be a dependently typed language for writing programs that you just want to run, but I would be delighted to be corrected on that viewpoint!