Andrew Wiles' Proof of Fermat's Last Theorem, As Expected, Does Not Require a Large Cardinal Axiom. A Discussion of Colin McLarty's "The Large Structures of Grothendieck Founded on Finite-Order Arithmetic"
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.