What makes dependent type theory more suitable than set theory for proof assistants?

In the Q&A part of the talk (at 1:00:00) he justifies this as follows:My question is about the first of these: Why is automation very difficult with set theory (compared to dependent type theory)?I apologize for writing a lengthy answer, but I get the feeling the discussions about foundations for formalized mathematics are often hindered by lack of information.I have used proof assistants for a while now, and also worked on their design and implementation. A second component of the proof assistant, the elaborator, translates $V$ to $F$ and passes the translations to the kernel for verification.A proof assistant may incorporate a third formal language $M$ (the meta-language), which is used to implement proof search, decision procedures, and other automation techniques. Since both set theory and type theory are mathematically very well understood, and more or less equally expressive, the choice will hinge on technical criteria, such as availability and efficiency of proof-checking algorithms.A much more interesting question is what makes the vernacular $V$ suitable.For the vernacular to be useful, it has to reflect mathematical practice as much as possible. On the other hand, $V$ should be a formal language so that the elaborator can translate it to the foundation $F$.To learn more about what makes $V$ good, we need to carefully observe how mathematicians actually write mathematics. Or to put it another way, as soon as we start expanding and transforming set theory to fit the requirements for $V$, we end up with a theoretical framework that looks a lot like type theory. (You may entertain yourself by thinking how set theory could be used to detect that $f : U \to V$ above does not make sense unless we insert coercions – for if everthying is a set then so are $U$ and $V$, in which case $f : U \to V$ does make sense.)An important aspect of suitability of foundation is its ability to detect mistakes. Nevertheless, a proof assistant whose foundation $F$ is based on ZFC will accept the above definition as valid, even though it is very unlikely that the human intended it.A proof assistant based on type theory would reject the definition by stating that "$U \in K$" is a type error.So suppose we use a set-theoretic foundation $F$ that accepts any syntactic formula as valid. But what is this additional mechanism, if not just a second kernel based on type theory?I am not saying that it is impossible to design a proof assistant based on set theory. But I cannot help to wonder: why bother with the set-theoretic kernel that requires a type-theoretic fence to insulate the user from the unintended permissiveness of set theory?I personally believe that the work Kevin Buzzard is doing is excellent; at the same time, he has strong opinions about proof assistants that are not universally shared, so you should take those opinions with a grain of salt.In 2018, John Harrison gave a talk entitled, Let's make set theory great again!. I am more than happy to engage with people in discussions about what I said and whether or not some things I said were ill-informed.But onto my answer to your question: whilst I am not an expert in proof assistants in general (I have become knowledgeable at precisely one proof assistant and have limited experience with others), it is my empirical observation that high-level tactics like Lean's ring tactic, which will prove results like $(x+2y)^3=x^3+6x^2y+12xy^2+8y^3$ immediately -- and there are similar tactics in Coq and Isabelle/HOL, two more type theory systems -- do not seem to exist in the two main set theory formal proof systems, namely Metamath and Mizar. My own direct automation experience is wrt to ACL2, Lean and SMT-based solvers.Strictly speaking, I don't know if there's any foundational argument for why set theory would be better or worse than the type theory-based approach in Lean.The strengths that Lean have from my perspective are: an expressive explicit type system, a relatively simple core language for representing terms, and a attention to how terms are represented for efficient manipulation.With regards to typed core logics, most automation in theorem provers is tailored to specific common theories that are widely used in mathematics. In this variety, type inference is decidable whilst in the extensional variety it is not.Set Theory like machine code, like assembly and like early programming languages are not typed.