I think the answer is yes. Modern efforts to formalize mathematics use type theory a lot, specifically calculus of inductive constructions, rather than ZFC. At

I think the answer is yes. Modern efforts to formalize mathematics use type theory a lot, specifically calculus of inductive constructions, rather than ZFC. At around 2000, I studied applied mathematics. I was curious about automated theorem proving, but I didn't understand the language (being, as most mathematicians, trained in proving with classical logic rather than type theory). Years later I discovered Haskell, which became a "gateway drug" to type theory. I wish something like Lean had existed 25 years ago, when I was a student. I think fully formal methods in mathematics are the future, and every math student should learn a bit of Lean (or a similar tool, but IMHO Lean has the best tutorials, aimed at people with traditional education). Hence, everybody should learn basics of type theory.