Inaccessible cardinals and Andrew Wiles's proof In a recent issue of New Scientist (16 Aug 2010), I was surprised to read that a part of Wiles' proof of Taniyama-Shimura conjecture relies on inaccessible cardinals.
Here's the article

*

*Richard Elwes, To infinity and beyond: The struggle to save arithmetic, New Scientist, August 2010.

Here's the relevant bit from the article:

"Large cardinals have been studied by logicians for a century, but their intangibility means they have seldom featured in mainstream mathematics. A notable exception is the most celebrated result of recent years, the proof of Fermat's last theorem by the British mathematician Andrew Wiles in 1994 [...]
To complete his proof, Wiles assumed the existence of a type of large cardinal known as an inaccessible cardinal, technically overstepping the bounds of conventional arithmetic"

Is this true ?
If so, could someone please outline how they are used ?
 A: The basic contention here is that Wiles' work uses cohomology of sheaves on certain Grothendieck topologies, the general theory of which was first developed in Grothendieck's SGAIV and which requires the existence of an uncountable Grothendieck universe.  It has since been clarified that the existence of such a thing is equivalent to the existence of an inaccessible cardinal, and that this existence -- or even the consistency of the existence of an inaccessible cardinal! -- cannot be proved from ZFC alone, assuming that ZFC is consistent.
Many working arithmetic and algebraic geometers however take it as an article of faith that in any use of Grothendieck cohomology theories to solve a "reasonable problem", the appeal to the universe axiom can be bypassed.  Doubtless this faith is predicated on abetted by the fact that most arithmetic and algebraic geometers (present company included) are not really conversant or willing to wade into the intricacies of set theory.  I have not really thought about such things myself so have no independent opinion, but I have heard from one or two mathematicians that I respect that removing this set-theoretic edifice is not as straightforward as one might think.  (Added: here I meant removing it from general constructions, not just from applications to some particular number-theoretic result.  And I wasn't thinking solely about the small etale site -- see e.g. the comments on crystalline stuff below.)
Here is an article which gives more details on the matter:

*

*Colin McLarty, What does it take to prove Fermat’s last theorem? Grothendieck and the logic of number theory, Bull. Symb. Log. 16 No. 3 (2010) pp. 359–377, doi:10.2178/bsl/1286284558, archived author pdf.

Note that I do not necessarily endorse the claims in this article, although I think there is something to the idea that written work by number theorists and algebraic geometers usually does not discuss what set-theoretic assumptions are necessary for the results to hold, so that when a generic mathematician tries to trace this back through standard references, there may seem to be at least an apparent dependency on Grothendieck universes.
P.S.: If a mathematician of the caliber of Y.I. Manin made a point of asking in public whether the proof of the Weil conjectures depends in some essential way on inaccessible cardinals, is this not a sign that "Of course not; don't be stupid" may not be the most helpful reply?
A: 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.
A: Can I draw attention to the continuation of that quotation? "But there is a general consensus among mathematicians that this was just a convenient short cut rather than a logical necessity. With a little work, Wiles's proof should be translatable into Peano arithmetic or some slight extension of it."
For the record, McLarty's paper in the Bulletin of Symbolic Logic was indeed the source for my claim that Wiles used an inaccessible cardinal (via Universes). If anyone fancies debating the exact definition of 'using' an axiom without 'needing' it, and whether or not that definition applies in the current case, we should probably do it somewhere else (Pedantry Overflow?). But I explicitly opposed the claim that the proof 'needed' large cardinal assumptions, so I don't propose to be too apologetic.
Anyway, it's an interesting question, and I'd be pleased if my article goes some way to bringing an answer into the public domain (even if I do get my head shot off in the process ;) ).
(Incidentally I would rather have left this as a comment than an answer, but don't have enough (any) reputation points. If anyone with superpowers wants to move it, please go ahead.)
A: There was some discussion about this on the FOM mailing list: see for example 
http://cs.nyu.edu/pipermail/fom/1999-April/002983.html,
where someone claimed Wiles needed in accessible cardinals, and Harvey Friedman essentially told them to stop being stupid. (Friedman is the guy who created the subject of reverse mathematics, which studies what axioms are necessary for any given result.)
An analogy would be the claim that classifying groups of order 4 needs Grothendieck universes, because groups of order 4 form a proper class, so isomorphism classes of groups of order 4 form a 2-class of classes. This is obviously silly: it is trivial to restate the classification of groups of order 4 without using proper classes, but this makes the statement slightly more complicated: you have to talk about groups that are hereditarily finite sets or something like that, which is just an irrelevant complication. The use of Grothendieck universes is similar: for example, the collection of all etale spaces over a scheme is a proper class so in some sense uses universes to construct it, but is equivalent to a much smaller set so the use of universes is not necessary. 
A: At the suggestion of François G. Dorais I am moving this answer from Recent claim that inaccessibles are inconsistent with ZF to here. The text below was written before I read the above, very well-informed answers/comments, so there is considerable overlap.

This is just a quick answer regarding FLT, mentioned by the OP.
Colin McLarty is working on showing a small part of Friedman's grand conjecture, namely that the Fermat-Wiles(-Taylor?) theorem is provable in a weak system of arithmetic. Since originally the semi-stable case of Taniyama-Shimura-Weil that Wiles proved (not to mention the work by others such as Frey, Serre, Ribet to get to that point) required large parts of algebraic and arithmetic geometry developed by the Grothendieck school, which among other things uses sheaves, cohomology and so on, and so a priori requires some foundational care. Universes (~inaccessible cardinals) were introduced to take care of the problem of e.g. forming categories of sheaves on categories of sheaves on a site.
However, one can use a version of set theory much weaker than ZFC+Universe(s), indeed a fair bit weaker than ZFC, as McLarty has shown, and still get pretty much all of EGA/SGA (this is based on general arguments, he hasn't sat down and worked through it all). However, the arithmetic geometry needed for FLT [edit: and indeed a lot of number theory] really only needs to consider countable sites, rather than generic small sites, and so one really only needs to assume much weaker assumptions about infinite objects.
A more recent talk (July 2011 - slides not publicly available as far as I know) by McLarty had the statement that derived functor cohomology is a finitely axiomatised first-order theory, and so not really the complicated logical beast it appears to be.
EDIT: More work has been published in the meantime:

*

*Colin McLarty, The large structures of Grothendieck founded on finite-order arithmetic, Rev. Symb. Log. 13 No. 2 (2020) pp. 296–325, doi:10.1017/S1755020319000340, arXiv:1102.1773
To quote from the abstract:

Such large-structure tools of cohomology as toposes and derived categories stay close to arithmetic in practice, yet existing foundations for them go beyond the strong set theory ZFC. We formalize the practical insight by founding the theorems of EGA and SGA, plus derived categories, at the level of finite order arithmetic.

Some partial results to getting to a specific finite order are in

*

*Colin McLarty, Zariski cohomology in second order arithmetic, arXiv:1207.0276

The cohomology of coherent sheaves and sheaves of Abelian groups on Noetherian schemes are interpreted in second order arithmetic by means of a finiteness theorem

though the tools in that paper are insufficient to apply to étale cohomology, this means we are a long, long way from needing universes.
