The current tittle of the original MathOverflow question is "What makes dependent type theory more suitable than set theory for proof assistants?", I don't know why is it different than here. The actual question makes more sense because the one on HN suggests that proof assistants exclusively formalize mathematics in dependent type theory (rather than set theory) which is not true. In fact, some proof assistants use dependent type theory (LEAN), some use simple type theory (Isabelle/HOL), some use simple type theory to encode untyped set theory (Isabelle/ZF), some implement kind of "soft typing" on top of untyped set theory (Mizar) and some are completely generic and can encode all of the above (Metamath).
As for the question why type theory seems to be more popular in formalization of mathematics recently than set theory Jeremy Avigad wrote a rare compelling explanation [1] of why this is the case. I personally prefer the opinion of Lawrence Paulson [2], the original author of Isabelle and its ZF logic (he also implemented a formalization of ZFC set theory in Isabelle/HOL recently).
> The current tittle of the original MathOverflow question is "What makes dependent type theory more suitable than set theory for proof assistants?", I don't know why is it different than here.
It's too long for HN, OP presumably reworded to fit. If you have a better suggestion one of the mods might see and change it, I think OP's chance to edit it has passed though.
[1] https://cs.nyu.edu/pipermail/fom/2016-January/019441.html
[2] https://cs.nyu.edu/pipermail/fom/2018-June/021032.html