> we have an upper bound

Is Wiles' proof even in ZFC?

I would be surprised if it wasn’t. Maybe some part of depends on the continuum hypothesis, but ZFC is pretty powerful

Your question is explored in https://www.cs.umd.edu/users/gasarch/BLOGPAPERS/fltlargecard...

Thanks. So if I read this correctly - there is consensus that Wiles' proof can be reduced to ZFC and PA (and maybe even much weaker theories). But as presented Wiles proof relies on Grothendieck's works and Grothendieck could not care less about foundationalism, so no such reduction is known and we don't really have a lower bound even for ZFC.

Even super simple results like uniqueness of prime factorisation can pages of foundational mathematics to formalise rigorously. The Principia Mathematica famously takes entire chapters to talk about natural numbers (although it's not ZFC, to be fair). For that reason I think it's pretty unlikely.