The issue is automation: At this point (Feb 2021), the support in interactive theorem provers is just much better for type-theory based mathematics in contrast

The issue is automation: At this point (Feb 2021), the support in interactive theorem provers is just much better for type-theory based mathematics in contrast to set-theory based maths. Whether that is due to technical advantages of type-theory over set theory, or a historical accident, reflecting the much larger amount of attention on type-theory as basis for interactive provers, is a subject of much controversy. Let me cite a leading light in the formalisation of mathematics [1]: "I would guess that the amount of effort and funding going into type theory exceeds the amount that went into set theory by an order of magnitude if not two [...] I am certain that we would now have highly usable and flexible proof assistants based on some form of axiomatic set theory if this objective had enjoyed half the effort that has gone into type theory-based systems in the past 25 years." Paper [2] has brought renewed attention to set-theory as a basis for automating mathematics. [1] https://cs.nyu.edu/pipermail/fom/2018-June/021032.html https://cs.nyu.edu/pipermail/fom/2018-June/021032.html [2] https://arxiv.org/abs/1707.04757 https://arxiv.org/abs/1707.04757