Comment by ux266478

> lean4 doesn't let them formalize results outside of zfc.

A small correction: Lean 4's native semantics are DTT, not ZFC. Formalizing results for TT is arguably easier, it's the default. But you can use it for any foundation, so long as you have an implementation.