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).
> 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.
> 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.
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).