[skissane]

Is the problem that human mathematicians have decided that classical logic + ZF(C) is the best framework for them–but it isn’t the best framework for computers?

Which raises an interesting philosophical question - do contemporary mathematicians mostly do things one way rather than another (i.e. classical logic instead of intuitionistic/paraconsistent/etc logic, ZF(C) set theory instead of alternative set theories or type theory or whatever, classical analysis instead of non-standard analysis, and so on) - because they’ve settled upon the inherently superior (easier, more productive) way of doing things - or is that just an accident of history? Could it be that in some alternative timeline or parallel universe out there, mathematics took some different forks in the road, and the mathematical mainstream ended up looking very different from how it does here?

[giraj]

I can't speak for kxyvr, but let me chime in as a mathematician who does formalise my theorems. There's no issue with representing various foundations (e.g. ZFC) on a computer -- for example, that's essentially what Lean/mathlib does, and it's working out great for them. A "problem" with ZFC, however, is that it's very low-level, meaning there's a large distance between the "informal" proofs which mathematicians carry out and communicate, and their corresponding formal proofs in ZFC. Accordingly, for a ZFC-based mathematician to start using proof assistants, they not only have to learn how to use a proof assistant, but also to translate (or expand/elaborate) their math into ZFC.

In other foundations, such as homotopy type theory (which is what the article is about), the distance between "informal" mathematical arguments and their formal counterparts is much shorter. This is why formalisation is widespread in the HoTT-community. Indeed, I believe Voevodsky worked on HoTT in order to have a foundation which was much closer to the mathematical practice in homotopy theory.

[TechBro8615]

I find these "fork in the road" questions endlessly fascinating, and that's exactly what I was getting at with my comment about the motivation for formalizing mathematics. And it doesn't just apply to math, but the whole "tech tree" of human history. How many seemingly arbitrary choices led us down a path that unknowingly diverged from some alternative future?

Last time I commented about this [0], I made some guy irrationally angry as he told me I sounded like I was 19 years old. And in an earlier comment [1], another guy took extreme offense to my questioning of the statement "with enough marbles, the discrete distribution behaves like a continuous distribution."

It seems there is some high priesthood of mathematics and physics that doesn't like when you ask these sorts of questions.

[0] https://news.ycombinator.com/item?id=35018407

[1] https://news.ycombinator.com/item?id=35201603

[skissane]

> Last time I commented about this [0], I made some guy irrationally angry as he told me I sounded like I was 19 years old

If people make comments like that, flag them and email dang ([e-mail]) and he’ll do something about them

> It seems there is some high priesthood of mathematics and physics that doesn't like when you ask these sorts of questions

In my personal experience, most professional mathematicians and physicists are open to questioning the foundations of their discipline, and deal charitably with doubters (even those who are coming from a place of misunderstanding).

I suspect most of the “high priests” you speak of aren’t actually professionals at all, just Internet randoms who (at best) know only slightly more than you do, and who know very little about the norms of civil dialogue