Comment by jfmc

Not a mathematician, but AFAIK ZFC is a valid foundation. Dependent types helps a lot with bookkeeping, but cannot prove more theorems.

Lawrence Paulson is a great person to clarify those topics (Isabelle/HOL is not based on types yet it can proof most maths).