[Tainnor]

This is missing the point. Modern mathematics textbooks, especially undergratuate ones, are written with set theoretic foundations. It requires a lot of effort to reformulate all of mathematics into equivalent formulations. That makes it harder to get buy-in from many working mathematicians, and it also makes the subject less approachable for, say, undergraduates.

[creata]

> Modern mathematics textbooks, especially undergratuate ones, are written with set theoretic foundations.

Yes, but only the foundations. A math undergrad doesn't actually care whether an ordered pair (a, b) is encoded as {{a},{a,b}} or as an instance of the product type, and they don't care whether the natural number 2 is encoded as the set {{},{{}}} or as a value S(S(Z)) of the inductive type of the natural numbers. Although if pressured to choose, I bet they'd prefer the latter, since it gets a lot closer to how everyone thinks of "ordered pairs" and "natural numbers".

Since mathematicians always work with higher-level abstractions anyway, I don't think the fact that the very lowest layer of these abstractions is set theory actually gets in the way of formalization efforts.

[zozbot234]

Modern math textbooks are based on naïve set theory, which can be quite feasibly modeled, even by structural foundations. It might require some effort at the lowest layer of formalization, but even then only as a one-time thing that's not going to impact the project as a whole.

[Tainnor]

That may very well be the case, but to a person starting out right now, those foundations seem to be lacking right now (or at least are not easily discoverable).

[andrepd]

Not quite. You're conflating two things: using set theory to talk about sets (what undergraduate math textbooks do) and using set theory to talk about everything (what ZFC foundations does).

[Tainnor]

In 99% of algebra textbooks you'll see a definition like "if G is a group and H is a subset of G, then we call H a subgroup if it is a group under the same operation." Then, the next thing you see is probably the theorem that "H is a subgroup of G if and only if it is a subset of G and gh^{-1} € H for all g, h € H". That's clearly using the language of set theory to talk about groups.

I mean, my argument is not that type theory or anything is unsuitable for doing maths. It's that it is different from how most people do maths. In my particular case, I am such an undergraduate who has actually tried to do some group theory in Coq and found it annoying to pull it off—not in the least because I figured out there were multiple equivalent ways of e.g. defining what is a group and/or subgroup and I had no idea which one was more natural or useful; you can work with injective homomorphisms, as someone else suggested, but you can also work with predicates so that you define a subgroup as all elements of some type that satisfy that predicate. Moreover, the fact that Coq includes several different types of "truth" (basically, Bool vs. Prop), which is undoubtedly well-reasoned, requires some adjustment, too.

Again, I'm not saying that this is a failure of tools such as Coq (although, they should really make documentation more discoverable and understandable). My sole argument was that you can't currently take any mathematician not particularly interested in logic or proof theory, especially not an undergraduate student, and expect them to encode simple proofs that they understand in Coq without a lot of assistance. If these tools are to be the future of (some part of) mathematics, they will have to become more accessible one way or another.

Ironically (?), I found that it was much easier to use Coq to prove e.g. algorithms correct (especially if you've done functional programming before) because programming languages actually do use types (even if some of them only do so at runtime).

[creata]

> That's clearly using the language of set theory to talk about groups.

If you like the language of set theory, what's wrong with replacing "A ⊆ X" with "A : SubsetOf X" where SubsetOf X = X → Prop? This is what Lean does: https://leanprover-community.github.io/mathlib_docs/group_th...

> there were multiple equivalent ways of e.g. defining what is a group and/or subgroup

Don't you have that problem in any foundation?

> Moreover, the fact that Coq includes several different types of "truth"

You probably know this already, but you can collapse Prop to Bool by adding some classical axioms.

> My sole argument was that you can't currently take any mathematician not particularly interested in logic or proof theory, especially not an undergraduate student, and expect them to encode simple proofs that they understand in Coq without a lot of assistance.

True, but I don't think that's a goal of the Coq developers right now. I feel like Lean is the only project trying to make formal proofs of classical mathematics accessible to an undergraduate student.

[andrepd]

> My sole argument was that you can't currently take any mathematician not particularly interested in logic or proof theory, especially not an undergraduate student, and expect them to encode simple proofs that they understand in Coq without a lot of assistance.

Oh but absolutely, I agree 100%. I consider it the "holy grail" of interactive proof assistants: an assistant that understands mathematics as written by humans in papers, plus is capable of filling in intuitively trivial/boring steps. In other words: an assistant that is usable by someone with training in mathematics but not necessarily requiring training in the tool itself.