What set-theoretic definitions can't easily be formalized in a type theory?

Andrej's answer that "Almost no pen-and-paper mathematics is written in ZFC" is correct. But it's perhaps also worth noting that some pen-and-paper mathematics is written in ZFC (or, at least, something closer to ZFC than to type theory), such as much of the mathematics done by set theorists (in which phrase, of course, "set" refers traditionally to a ZFC-set).

A good deal of set theory can be rephrased more structurally to make sense in type theory, but this would be a rephrasing, and the amount of work that would be required is, I think, variable. For instance, set theorists work with ordinals defined in the von Neumann way, with $\in$ as the well-founded relation. This in particular implies that ordinals are literally unique representatives of isomorphism classes of well-ordered sets. In type theory it is more natural to work "structurally" with arbitrary well-ordered sets rather than with von Neumann ordinals. This makes some things more cumbersome because of isomorphisms that get carried around (although under univalence, these isomorphisms become equalities), but probably doesn't change things a whole lot.

On the other hand, as far as I know, no one has ever come up with a convincing structural presentation of Godel's constructible universe $L$. The only structural approaches to $L$ that I know of essentially involve building a model of ZF(C) in some way and then constructing $L$ inside that model. Note that $L$ is, as far as I know, still the only way to prove the relative consistency of the Axiom of Choice, so it is of interest even to mathematicians who don't care about ZF for its own sake. (In contrast, the symmetric/permutation methods used to prove relative consistency of not-AC, and the forcing methods that can be used to prove consistency of other properties such as GCH and not-GCH, seem much more amenable to structuralization.) [Note: this paragraph was edited to remove a false claim that GCH is not forceable; see comments.]

As another example, Scott's trick is a method used in pen-and-paper mathematics that is of interest beyond set theory, but relies on the axiom of foundation from ZFC, and so is not obviously formalizable in type theory.

Type theory seems to have a bit of difficulty with partial functions in practice. Since total functions are the primitive concept, you have to code partial functions somehow. I've seen the following approaches:

• Use some specific junk value (e.g., 2 - 3 = 0 : ℕ and 1 / 0 = 0 : ℚ).
• Use an undefined junk value (i.e., 1 / 0 is a term of the appropriate type, but you can't prove anything about its particular value). (This is the approach sometimes used in Isabelle/HOL with its undefined term.)
• Use a maybe/option monad. In other words, rather than having subtraction on ℕ be a function of type ℕ → ℕ → ℕ, you have it be a function of type ℕ → ℕ → ℕ ⊕ Unit, using () : Unit as your undefined value.
• Use something like Lean's PFun monad. So now subtraction on the naturals would be a function of type Σ a b : ℕ, Σ p : a ≥ b, ℕ, which takes two inputs a and b and a proof p that a is greater than or equal to b and then produces a - b : ℕ. (Or something like this. This isn't literally what Lean's PFun monad does, but it's essentially equivalent.)
• Use side conditions or subtypes (which is what's used in PVS). These are formally quite similar to the PFun approach, but are a bit different from an end-user perspective.

The last three are obviously more 'conceptually correct' but they're enough of a hassle that the first approach is fairly common. (I think Rocq, Agda, Lean, and Isabelle/HOL all have 2 - 3 = 0 : ℕ, for instance.) This leads to its own issues though, as discussed by Loeffler and Stoll in Section 5 of Formalizing zeta and L-functions in Lean. They had to perform a (in their words) "lengthy and quite delicate computation" to establish that Lean's definition of the Riemann zeta function satisfies $\zeta(1) = \frac{1}{2}(\gamma - \log 4\pi)$ in order to show in particular that Lean's value of $\zeta(1)$ didn't make certain statements of the Riemann hypothesis trivially false (since in principle it might have been the case that $\zeta(1) = 0$). This result is now a named theorem in Mathlib, specifically riemannZeta_one. So, in other words, the difficulty with talking about partial functions directly eventually necessitated the inclusion of a mathematically non-trivial junk theorem in Mathlib.