Fermat's Last Theorem

That xⁿ + yⁿ  zⁿ has no integer solutions for n > 2 was suggested by Pierre Fermat around 1665. Fermat proved this for n = 4 around 1660; Leonhard Euler for n = 3 around 1750. It was proved for n = 5 and n = 7 in the early 1800s. Then in 1847 Ernst Kummer used ideas of factoring with algebraic integers to prove it for all n < 37. Extensions of this method gradually allowed more cases to be covered, and by the 1990s computers had effectively given proofs for all n up to several million. Meanwhile, many connections had been found between the general case and other areas of mathematics—notably the theory of elliptic curves. And finally around 1995, building on extensive work in number theory, Andrew Wiles managed to give a complete proof of the result. His proof is long and complicated, and relies on sophisticated ideas from many areas of mathematics. But while the statement of the proof makes extensive use of concepts from areas like set theory, it seems quite likely that in the end a version of it could be given purely in terms of Peano arithmetic. (By the 1970s it had for example been shown that many classic proofs with a similar character in analytic number theory could at least in principle be carried out purely in Peano arithmetic.)