I'm writing a new community wiki answer because it seems to me the consensus in the comments is that the accepted answer doesn't really tell the right story, and since this is something that pops up all the time it'd be good to have a single place to point people without making them read through all the comments. Please improve my answer.

In the most naive sense Wiles proof does depend on existence of Grothendieck universes (and thus on existence of inaccessible cardinals). By this I mean if you took every reference in Wiles proof and read the first published proof of that fact you'd certainly end up somewhere in SGA where, due to Grothendieck's love of generalization, you'd find universes popping up.

However, this certainly doesn't mean the proof really uses universes. It's widely believed (though for some people this belief may not come from much direct evidence) that in any practical situation you don't actually need universes. However, there are some concrete situations (BCnrd mentions some involving sheafification on the crystalline site) where it's not necessarily known how to eliminate the use of universes.

As a result, in order to figure out if Wiles's proof uses universes, or whether it's relatively easy to avoid them, you'd need to either read the proofs yourself or find someone who was both deeply familiar with the details of the proof, and someone who cares a lot about details. One person who comes quickly to mind is BCnrd. BCnrd was one of the mathematicians who proved the Modularity Theorem, which showed that all elliptic curves over $\mathbb{Q}$ are modular. This is a strengthening of Taylor and Wiles' result, which applied only to semi-stable elliptic curves, and the proof involved understanding and building on Taylor and Wiles' work. BCnrd is also famous for his attention to detail and for consulting underlying foundational sources; he is the author of a book dedicated to simplifying and correcting the presentation of Grothendieck duality in Hartshorne's book *Residues and Duality*.

As explained in the comments to Pete's answer, BCnrd says there's really no issue at all in Wiles's proof. All of the specific things that Wiles uses stay far away from any of the difficult issues where you might be worried about needing to invoke universes.

generaltheory of cohomology onalltopoi, including operations like sheafification, enough injectives, derived categories, and Ext-sheaves, there needs to be a way to control the "size" of coverings which arise in these constructions (to replace the implicit role of "power set" for ordinary topology spaces). The universe stuff takes care of such matters in an elegant way, so one can focus attention on the more central aspects of the theory. $\endgroup$ – BCnrd Aug 17 '10 at 5:436more comments