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.