I still find it very surprising that this random talk I gave attracts so much attention, especially as not everything I said was very well thought out. 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 higher-order 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. I don't really know why, but those are the facts.

I still find it very surprising that this random talk I gave attracts so much attention, especially as not everything I said was very well thought out. 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. I don't really know why, but those are the facts. Note that the proof of this from the axioms of a ring is extremely long and uncomfortable, because you need to apply associativity and commutativity of addition and multiplication many times -- things mathematicians do almost without thinking.