  Andrew Wiles' proof of Fermat's Last Theorem, with an assist from Richard
Taylor, focused renewed attention on the foundational question of whether the
use of Grothendieck's Universes in number theory entails that the results
proved therewith make essential use of the large cardinal axiom that there is
an uncountable strongly inaccessible cardinal, or more generally, that every
cardinal is less than a strongly inaccessible cardinal. If one traces back
through the references in Wiles' proof, one finds that the proof does depend
upon explicit use of Grothendieck's Universes. Thus, prima facie, it appears
that the proof of Fermat's Last Theorem depends upon a foundation that is
strictly stronger than ZFC. Colin McLarty removes this appearance by
demonstrating that all of Grothendieck's large tools, i.e., entities whose
construction depended upon Grothendieck's Universes, can instead be founded on
a fragment of ZFC with the logical strength of Finite-Order Arithmetic. The
goal of this article is to present overviews both of the history of Fermat's
Last Theorem and of McLarty's foundation for Grothendieck's large tools.
