I had promised myself that I had already said my last word on this question, but I want to tie up at least a few of the loose ends. Everyone is welcome to continue to comment while I move on to other topics.
I apologize to Dimitris if I took his comments out of context, but I have been reading them over and over for the last half hour and I don’t see how they could possibly mean anything other than what I thought they meant. I have also tried to read the previous posts but was stymied by the analytic/synthetic jargon that I have never encountered in mathematics and doesn’t seem to have much to do with the Kantian distinction.
(By the way, if I were Rick Deckard sitting in a bar in Blade Runner and I heard the person next to me say “I certainly do not claim that the notion of a set is objectively clearer than that of an ∞-groupoid” then I would begin to get nervous. Of course we may wonder what the word “objective” has to do with ZFC, but someone who has never owned a set of dishes or stayed at a club for the last set or, if the ambient language happened to be German, had never heard this song, is almost certainly a replicant. I like to reserve the word “objective” for the objects of our shared human perceptual environment, and in this sense the notion of a set is adapted to our sense of objectivity in a way that a Grothendieck topology doesn’t seem to be. Learning how to use Grothendieck topologies was worth the trouble because it answered specific questions of interest. Whether the same can be said of replacing sets by types remains to be seen.)
Lenstra’s comment was probably meant as a joke, or as a rhetorical flourish. He was well aware that, twenty years before he wrote those words, Mazur had announced his proof of the bound on torsion of elliptic curves over Q, and he did it by representing a functor and closely studying the geometry of the result. As a rule, mathematicians don’t realize that their offhand remarks are frequently read as philosophical position statements. I deliberately wrote much of my book in an elliptical style, in order to avoid misunderstandings; of course, the result is a different kind of misunderstanding.
I’m sure Dimitris sincerely believes that “no reasonable practicioner/admirer of HTT that I know of is trying to convince anyone to abandon the way they think of things, especially number theorists and other practicing mathematicians.” I quote Voevodsky in Part 2 asserting that “these foundations [HOTT/UF] will soon replace set theory.” In my book I quote his prediction (in 2011) that within five years no journal would publish papers not accompanied by a machine-verifiable equivalent. There are a number of similar comments in my book and in my chapter in Circles Disturbed. I think the expression “militant enthusiasm” is in many cases an accurate description of this attitude. (Tim Gowers predicts that computers will have replaced human mathematicians by 2099; but he’s not a militant enthusiast; he writes that he’s “not particularly happy” at the prospect.)
The most interesting point of contention is one that has nothing to do with HOTT or automated proof-verification or theorem-proving. Dimitris writes that logic
is detached from “real” mathematics because its object of study *is* “real” mathematics (rather than the object of study *of* “real” mathematics).
I have no objection to this sentence if by “‘real’ mathematics” Dimitris means an idealized and formalized simulacrum of human mathematics. If, however, the mathematics of practicing mathematicians is seen as an imperfect approximation to the “real” mathematics of formal systems, then we have a philosophical disagreement. Too many philosophers of mathematics hold this position (and philosophers who see things differently have a very hard time getting jobs); I don’t know what logicians believe. My own position is stated in Chapter 3:
Unlike those of my colleagues who predict that computers will soon replace human mathematicians by virtue of their superior skill and reliability in proving theorems, I am inclined to respond that the goal of mathematics is to convert rigorous proofs to heuristics. The latter are in turn used to produce new rigorous proofs, a necessary input (but not the only one) for new heuristics.
I had one more comment in response to Tim Campion. He wrote that
Univalence says that isomorphic things are equal.
Of course I have already seen that, but I don’t know what that entails (when representing functors, for example). It seems to be related to his later comment:
If you have to work with (higher) groupoids, currently you have to go read something like the Stacks project or Lurie’s book, learn a kind of elaborate formalism, and develop a whole suite of intuitions about the right ways to formulate statements about higher groupoids that are going to be correct and provable, and you have to learn lots of technical details about how to go about actually proving such statements. With the utmost respect to the authors of existing texts, this is a somewhat painful and time-consuming process.
I am actually in the throes of just such a process, and while I think the Stacks project is pretty good for a 4000-page manuscript, I would naturally like to save time and avoid pain. But a lot of hard work has gone into proving the theorems in the Stacks project and Lurie’s books, and I seriously doubt that introducing new foundations will simply make that work go away.