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.
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.
I would be surprised if it wasn’t. Maybe some part of depends on the continuum hypothesis, but ZFC is pretty powerful