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