Type theory has advantages over set theory for the (computer) formalisation of mathematics, but has anybody who does mathematics with pen and paper found proof assistants or automated theorem provers, such as Lean or Coq or Agda, to be 'ergonomic' enough that felt that they could move to doing their mathematics on the computer by default?
A related question is whether it might be easier to learn certain mathematical concepts with naive set theory than it might be with intuitionistic type theory, irrespective of the fact that typing is more or less ubiquitous in traditional mathematics in a broad sense of the term, e.g., "Let $n\in\mathbb{N}$".
