[ImprobableTruth]

>the experts in foundations don't seem to think highly of it.

Feel free to name some of these experts. The only thing I've seen is remarks by generally renowned mathematicians such as Terry Tao who have no interest in either foundations or formal verification (which isn't an indictment, its quite removed from mainstream mathematics), so I don't see why anyone would use this to evaluate the merit of HoTT.

>Many arguments for its utility or theoretical importance are, in my opinion, misguided – for example, the claim that set theory proves "junk theorems" such as "pi" being an element of "4."

What? Either whoever said that has no clue what they're talking about or you are misremembering their argument. No, set theory doesn't allow you to prove that pi is an element of 4 - but it allows you to state it. And this is actually an issue in so far as that when you want to state actually meaningful theorems, you constantly have to make assertions about what an object is actually supposed to be. If you do this in a formalized, machine amenable way you just end up with a form of type theory.

And this isn't actually an argument in favor of HoTT, but just some form of (dependent) type theory, all of which essentially run along the lines of 'This makes proof assistants better/easier to use'. I've never heard a legitimate argument for why dependent type theory is overhyped - even hardcore Isabelle folks will have a hard time disputing that dependent type theory has made much more noteworthy recent advancements.

The main argument (from the point of general proof engineering) for HoTT is computable univalence i.e. being able to transfer properties along isomorphisms without the computation getting stuck which is a huge deal. Is it a large enough deal that everyone will adopt it? Who knows, it might be that a more 'practical' proof assistant such as Lean, focusing simply on better automation engineering, will win out, but the hype around HoTT is definitely not just a 'meme'. People over hyping category theory doesn't invalidate the actual research being done.

[spekcular]

> Feel free to name some of these experts.

Harvey Friedman and Steve Simpson have been quite vocal about it on the Foundations of Mathematics mailing list, for example. There are many others.

> What? Either whoever said that has no clue what they're talking about or you are misremembering their argument.

People definitely say this. See, for instance: https://mathoverflow.net/questions/90820/set-theories-withou.... And note that not just the questioner but also many commenters assent to that claim. See also the paper Set Theory and Structures by Barton and Friedman, starting p. 15: http://philsci-archive.pitt.edu/14633/1/2017_04_set_theory_u....

I will leave it up to you to decide whether they know what they're talking about.

> No, set theory doesn't allow you to prove that pi is an element of 4 - but it allows you to state it. And this is actually an issue in so far as that when you want to state actually meaningful theorems, you constantly have to make assertions about what an object is actually supposed to be. If you do this in a formalized, machine amenable way you just end up with a form of type theory.

I am not totally sure about the distinction you are trying to draw here. But I reject the claim that, properly understood, ZFC allows you to prove or state such a thing.

What ZFC does is allow one to reformulate all mathematical questions as questions about sets. So if I want to ask some question, like is pi^2 rational, then I can define Dedekind cuts, define squaring, and I know its truth value is the same as a certain question about sets of rational numbers.

Now, of course pi is not, philosophically speaking, the same as the set used to encode it. (And in fact there are many ways to do this encoding.) So one cannot even state questions like "Is 3 a member of pi?" in set theory, because 3 and pi are not sets. On the other hand, it is perfectly legitimate to ask questions like, "Is (the pair of natural numbers representing the number) 3 a member of the Dedekind cut associated with pi?"

> The main argument (from the point of general proof engineering) for HoTT is computable univalence i.e. being able to transfer properties along isomorphisms without the computation getting stuck which is a huge deal.

If my concern is studying the foundations of mathematics, I have not seen a reason why I ought to prefer HoTT over ZFC. But there are various reason to prefer the second, for instance the fact that at some point sets need to get into the picture anyway to give a satisfactory account (e.g. to define large cardinals to study the relative consistency strength of various theories).

If my concern is formalizing mathematics, Lean seems to be doing a much better job (see https://xenaproject.wordpress.com/2020/02/09/where-is-the-fa...). And HoTT gets something like 10x more attention than Lean does on HN. So I think "meme" is an apt description.

[ImprobableTruth]

The FOM folk are in general incredibly bearish on proof assistants, so of course they don't care. If you only care about an 'ultimate' foundation that is the best fit to evaluate other systems, rather than a foundation that is amenable to actively working with it, of course you have no reason to care about HoTT.

If you share their opinion, alright, but I personally find this incredibly myopic.

>People definitely say this. See, for instance: https://mathoverflow.net/questions/90820/set-theories-withou.... And note that not just the questioner but also many commenters assent to that claim. See also the paper Set Theory and Structures by Barton and Friedman, starting p. 15: http://philsci-archive.pitt.edu/14633/1/2017_04_set_theory_u....

I haven't read through all comments, but as far as I see people are actually just criticizing that the encoding is always relevant - that is, they can't talk about objects without encodings, but they don't actually care about the theorems regarding the encoding itself. I think this is fundamentally different from saying 'set theory proves 4 is an element of pi' because otherwise you could levy the same criticism against type theory! After all, there's nothing preventing people from encoding the natural numbers as sets in type theory. The benefit of type theory is that instead you can talk about objects without regard for the encoding which isn't possible with ZFC.

>I am not totally sure about the distinction you are trying to draw here. But I reject the claim that, properly understood, ZFC allows you to prove or state such a thing. >Now, of course pi is not, philosophically speaking, the same as the set used to encode it. (And in fact there are many ways to do this encoding.) So one cannot even state questions like "Is 3 a member of pi?" in set theory, because 3 and pi are not sets.

I guess it matters on how you view it exactly. Under your view you can't state it, but this comes at the cost of not being able to make any at all statements about objects rather than just specific encodings! I'd wager that the vast majority of people would be unsatisfied with this for actively doing mathematics. When people want to talk about the natural numbers, they don't actually care about the specific encoding, they just want to talk about the objects.

The way I see it, if I want to talk about the objects 4 and pi in set theory, I have to consider an arbitrary set that encodes it. Now, because these are still just sets, I can state '4 is an element of pi', but not prove it, because whether it's actually true depends on the specific encoding. This isn't great either, but I think this is a lot closer to how people actually work.

>If my concern is studying the foundations of mathematics, I have not seen a reason why I ought to prefer HoTT over ZFC.

When studying foundations itself ZFC is king, but no one is contesting that. Even HoTT fanatics will admit that its complexity makes it less amenable for certain situations.

>If my concern is formalizing mathematics, Lean seems to be doing a much better job

I'm not sure I understand. So you _do_ accept intuitionistic type theory as a valid alternative to ZFC when one actually wants to formalize mathematics?

Then your dislike of HoTT is even more confounding to me. HoTT is just an extension of intuitionistic type theory. If there's a mature HoTT implementation that stands the test of time (e.g. potentially a fully fleshed out version of cubical type theory), Lean is almost certainly going to incorporate it. Univalence is very much part of 'natural' reasoning, if I show a property for one encoding, I want to be able to transfer that to any other encoding. There's even already an experimental library for Lean that allows you to use univalence. It's just that generally Lean is a lot more conservative rather than experimental. They're not doing a better job because their theoretical foundation is better - it's simply that Kevin Buzzard and his troop is actually putting in the work of doing a lot of formalization.

>And HoTT gets something like 10x more attention than Lean does on HN.

Because HoTT is actually experimental research that could be a breakthrough for intuitionistic type theory, whereas Lean is 'just' people formalizing existing mathematics. I'm actually rather surprised that Kevin Buzzard's work is so popular here - he's certainly doing great work, but there hasn't really been any significant news for the past years. Not only that, but HN isn't a mathematics forum - his work seems about as popular as Coq and Agda here, even though the latter have a far more material impact on software engineering. HoTT is uncharacteristically popular as well, but at the very least there's a chance that it could change the face of formal verification!

[spekcular]

> The FOM folk are in general incredibly bearish on proof assistants, so of course they don't care. If you only care about an 'ultimate' foundation that is the best fit to evaluate other systems, rather than a foundation that is amenable to actively working with it, of course you have no reason to care about HoTT.

> If you share their opinion, alright, but I personally find this incredibly myopic.

I want to distinguish between two senses of "foundation of mathematics":

1) An ontologically minimal language to formalize mathematical reasoning and facilitate proving things about (in)consistency, provability, and relative theory strength, and generally doing metamathematics.

2) A language to actually carry out the details of formalizing mathematics, perhaps jointly by humans and computers, in the sense of the Xena Project and proof assistants.

Here is a claim which might annoy you, but really ought to be uncontroversial: the correct meaning of the term "foundation of mathematics" is the first one. This is what it has meant for about a hundred years, at least, and what someone working professionally in the reverse mathematics/set theory/model theory/logic communities will understand the phrase to mean if you use it in conversation with them.

Now, given this, and given you agree that ZFC does a better job at function (1) above, I think this explains why the FOM people (and more generally those in the communities I listed) find it strange when HoTT is suggested as a "foundation of mathematics." (I can't speak to their opinions on proof assistants, though.) You can see this quite explicitly when Harvey Friedman starts asking questions of the HoTT people; he always asks something about ontological parsimony, remarks how simple the ZFC axioms are (and tells a story about explaining them to his barber, or whatever), and remarks how homotopy is much too sophisticated a concept to be truly foundational.

Moreover, they are going to regard any criticism that ZFC is deficient because it's a poor choice for function (2) as totally besides the point. That's akin to arguing that Turing machines are a poor choice for the foundations of computational theory because it's hard to program them in practice. The same response to applies to your second point about how type theory is "closer to how people actually work"; this was never a figure of merit in the first place.

So, I indeed share this view, but I don't think it's myopic. I think it follows immediately from what a "foundation of mathematics" is.

> I'm not sure I understand. So you _do_ accept intuitionistic type theory as a valid alternative to ZFC when one actually wants to formalize mathematics?

Yes, with the caveat noted below. The practical formalization of mathematics is an engineering problem, not properly speaking one of foundations, as discussed above. This is not to say it's not a deep and interesting problem, just that the difficulties there are mostly orthogonal to those encountered when doing, e.g. metamathematics. One ought to do whatever makes formalization easiest for practitioners.

> Because HoTT is actually experimental research that could be a breakthrough for intuitionistic type theory

This is not compelling to me because I think intuitionism is boring and misguided. I think the majority of practicing mathematicians feel the same way. Of course, you can just add axioms to make it classical, but I'd wager the emphasis on intuitionism is another thing that turns people off from HoTT.

> I'm actually rather surprised that Kevin Buzzard's work is so popular here - he's certainly doing great work, but there hasn't really been any significant news for the past years.

He and his crew have actually formalized a good chunk of real mathematics. That's fairly significant, in my mind.

(You have probably already read this, but in case someone reading this post doesn't know what I mean: https://xenaproject.wordpress.com/2020/02/09/where-is-the-fa....)

Also, given that it's an engineering problem, there are going to be a bunch of difficulties that only pop up once you start playing with it. So the fact that a group of people have started playing with it, and found some of these problems, and iterated Lean in response – that's good!

[ImprobableTruth]

>Here is a claim which might annoy you, but really ought to be uncontroversial: the correct meaning of the term "foundation of mathematics" is the first one.

I know some people have advocated for different terms ('practical foundation of mathematics', 'framework of mathematics') but none of them seem to stick, so linguistic prescriptivism strikes me as a waste of time, especially with how overloaded terminology is in mathematics. Any arising confusion is unfortunate, but as long as it's clear what people mean, I don't see the issue and anyone who actually is able to differentiate between (1) and (2) should be able to understand what is meant from context.

>You can see this quite explicitly when Harvey Friedman starts asking questions of the HoTT people; he always asks something about ontological parsimony, remarks how simple the ZFC axioms are (and tells a story about explaining them to his barber, or whatever), and remarks how homotopy is much too sophisticated a concept to be truly foundational.

Sure and if this was the aim of HoTT, dismissing it for this reason would be legitimate, but it's not, as one can see by the reaction of HoTT people to these question: They'll deflect to (2) and do some spiel about 'entrances', because that's what they care about and refer to.

>Moreover, they are going to regard any criticism that ZFC is deficient because it's a poor choice for function (2) as totally besides the point. That's akin to arguing that Turing machines are a poor choice for the foundations of computational theory because it's hard to program them in practice. The same response to applies to your second point about how type theory is "closer to how people actually work"; this was never a figure of merit in the first place.

Then why are there so many people arguing for ZFC as an option for (2)? Not only are there proof assistants based on ZFC and people who advocate for this, a lot of the inane ZFC vs ETCS or HoTT discussions on FOM are absolutely about (2). Hell, even Harvey Friedman has engaged often enough in this e.g. arguing that the ability to make nonsensical statements is actually good because mathematicians start their work by making statements that are often nebulous or wrong.

>So, I indeed share this view, but I don't think it's myopic. I think it follows immediately from what a "foundation of mathematics" is.

I'm specifically talking about their views on matters of (2). If your criticism of HoTT is just that they're using the term 'foundation of mathematics' wrong, I'd say the HoTT folks are doing pretty well.

>Yes, with the caveat noted below. The practical formalization of mathematics is an engineering problem, not properly speaking one of foundations, as discussed above. This is not to say it's not a deep and interesting problem, just that the difficulties there are mostly orthogonal to those encountered when doing, e.g. metamathematics. One ought to do whatever makes formalization easiest for practitioners.

Are you referring to the development and study of formal systems such as CIC/intuitionistic type theory/HoTT or the actual development of proof assistants that implement these formal systems (Coq, Agda, Lean, etc)? Calling the former engineering seems quite strange to me and I don't see how you could reasonably claim that it's not metamathematics.

>This is not compelling to me because I think intuitionism is boring and misguided. I think the majority of practicing mathematicians feel the same way. Of course, you can just add axioms to make it classical, but I'd wager the emphasis on intuitionism is another thing that turns people off from HoTT.

Intuitionism is important for formal verification. For classical reasoning you can just - as you mention - add an axiom, which is also exactly what Lean does. If people dislike HoTT because it's not classical then that's just the fault of bad marketing. It's not indicative of the actual merits of HoTT at all.

>He and his crew have actually formalized a good chunk of real mathematics. That's fairly significant, in my mind.

It's significant and needed work, but there hasn't been any significant news for non-mathematicians. From the point of someone not familiar with mathematics, they've essentially been doing the same thing for about four years.

[spekcular]

> Any arising confusion is unfortunate, but as long as it's clear what people mean, I don't see the issue and anyone who actually is able to differentiate between (1) and (2) should be able to understand what is meant from context.

I don't think this is true at all! For example, maybe it is the case that HoTT proponents care solely about (2), and not (1), in which case my criticisms are misguided. But this is not at all the impression I get from reading what they write. Given I'm sensitive to the distinction between (1) and (2), and given I apparently can't infer the difference from context, what are we to conclude? That I just have poor reading comprehensions skills? Maybe so – in which case please help people like me out and use more precise terminology.

OK, I'm being a little coy here, but to be completely serious, I think it's already a confusing enough topic and a bunch of pointless debates could be avoided with better terminology.

> Sure and if this was the aim of HoTT, dismissing it for this reason would be legitimate, but it's not, as one can see by the reaction of HoTT people to these question: They'll deflect to (2) and do some spiel about 'entrances', because that's what they care about and refer to.

I went back to the introduction to the HoTT book [0] to check, to make sure I'm not misremembering things. And they literally say: 'we therefore believe that univalent foundations will eventually become a viable alternative to set theory as the “implicit foundation” for the unformalized mathematics done by most mathematicians.'

This can't be sense (2), because it refers to "unformalized mathematics." So it has to be sense (1). And this is not the only sentence of this kind, e.g., 'This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an “invariant” conception of the objects of mathematics.'

> Then why are there so many people arguing for ZFC as an option for (2)? Not only are there proof assistants based on ZFC and people who advocate for this, a lot of the inane ZFC vs ETCS or HoTT discussions on FOM are absolutely about (2). Hell, even Harvey Friedman has engaged often enough in this e.g. arguing that the ability to make nonsensical statements is actually good because mathematicians start their work by making statements that are often nebulous or wrong.

Yeah, I agree with you. There's no a priori reason to believe ZFC is a good choice for this.

> Are you referring to the development and study of formal systems such as CIC/intuitionistic type theory/HoTT or the actual development of proof assistants that implement these formal systems (Coq, Agda, Lean, etc)? Calling the former engineering seems quite strange to me and I don't see how you could reasonably claim that it's not metamathematics.

Well, metamathematically speaking, the development and study of these formal systems is boring. They don't have anything interesting to say about consistency or provability or whatever, and (as I understand it) they're all mutually intepretable with ZFC (at least the versions used to actually formalize things in practice). So whatever you want to call it, this research is not really justifiable on traditional metamathematical grounds. The actual point seems to be facilitating the construction of proof assistants.

> It's significant and needed work, but there hasn't been any significant news for non-mathematicians. From the point of someone not familiar with mathematics, they've essentially been doing the same thing for about four years.

I'm not sure what "there hasn't been any significant news for non-mathematicians" means here. For example, Quanta articles on various mathematical discoveries and sociological phenomena (from chalk to disagreements over the foundations of symplectic topology) routinely get posted on HN and are well received. If this is the bar for "significant for a non-mathematician," then I think finally formalizing a good chunk of "fashionable" mathematics is absolutely newsworthy. For a long time many people didn't take formalization seriously because it never touched "real" math, and now you're telling me I can do "real" math with it? To the point where undergrads are formalizing the standard undergrad/grad curriculum? That's huge!

[0] https://hott.github.io/book/nightly/hott-online-1287-g1ac940...

[ImprobableTruth]

>OK, I'm being a little coy here, but to be completely serious, I think it's already a confusing enough topic and a bunch of pointless debates could be avoided with better terminology.

Sure, I just don't think it's going to happen. The HoTT (and category theory) people largely don't care about (1), so they typically don't need to differentiate. More cynically, it's probably also just better marketing, a new 'foundation' certainly sounds more impressive than just a new 'mathematical framework', especially because (1) is generally pretty esoteric.

>This can't be sense (2), because it refers to "unformalized mathematics." So it has to be sense (1).

I don't think so, look at how they actually define 'unformalized mathematics':

"Indeed, many of the proofs described in this book were actually first done in a fully formalized form in a proof assistant, and are only now being “unformalized” for the first time — a reversal of the usual relation between formal and informal mathematics."

The idea is essentially that using HoTT formalisms informally can lead to new insight, which is exactly what part 2 of the book focuses on and they're making it clear that it's about general mathematics rather than metamathematics. If they were talking about (1), you'd expect them to at least do some actual metamathematics with it!

I think your next sentence actually serves to support this further.

>And this is not the only sentence of this kind, e.g., 'This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an “invariant” conception of the objects of mathematics.'

And now consider how the sentence actually ends "- and convenient machine implementations, which can serve as a practical aid to the working mathematician". You could argue that it being a practical aid only refers to the convenient machine implementations, but how would 'homootopical content' or 'an "invariant" conception' remotely help with (1)? To me this makes it pretty clear that the aim is to have a practical 'foundation' for the average working mathematician i.e. (2).

>So whatever you want to call it, this research is not really justifiable on traditional metamathematical grounds. The actual point seems to be facilitating the construction of proof assistants.

Sure, that I don't disagree with, it's definitely in the area of 'applied metamathematics' and there's a reason type theory field is more on the CS side. I just think that you would generally get some pretty strange looks if you called e.g. research on sequent calculus an 'engineering problem', even though it's typically done with the intent of eventually getting a practical system.

>I'm not sure what "there hasn't been any significant news for non-mathematicians" means here. For example, Quanta articles on various mathematical discoveries and sociological phenomena (from chalk to disagreements over the foundations of symplectic topology) routinely get posted on HN and are well received. If this is the bar for "significant for a non-mathematician," then I think finally formalizing a good chunk of "fashionable" mathematics is absolutely newsworthy

My point is that often there has been no 'visible' (for a non-mathematician) progress made, so it's curious to me that despite this it still gets posted here every few months. I would have expected some attention if some larger milestone was reached (e.g. formalizing most of an undergrad degree), it's the consistency that is surprising to me.