The Chimerical Effort to Seek Certainty
Mark Twain suggested the lovely notion of a “Sunday truth”: something fervently believed in church on Sunday but having no effect on behavior in the rest of the week. Many mathematicians will profess a belief in formalism when foundational matters are discussed. But in their day-to-day work as mathematicians, they remain thoroughgoing Platonists. The “crisis” in foundations from the turn of the 20th century to the 1920s has quietly dissipated. Set theory as a foundation is evident in the initial chapter of many graduate-level textbooks. The obligation to always point out a use of the axiom of choice is a thing of the past. I haven’t heard of anyone calling the proof of Fermat’s Last Theorem into question because of the large infinities implicit in Grothendiek universes. But there are those who wish to draw a line between safe and unsafe proof methods. The line is drawn by some who insist on some variety of constructivity. Others demand predicativity. Contemporary foundational research makes such notions precise and obtains theorems on the relative strengths of different methods. But there is no pointless attempt to restrict mathematicians. History suggests that they will use whatever methods work including the higher realms of the infinite.
-  Number theorists regard the use of Grothendiek universes as a mere convenience. See  for acareful discussion.