[cubefox]

> The question still is whether "folk theorems" are real. Certainly Cantor's theorem is no such folk theorem, as you have just been given a fully formal proof.

I didn't say that Cantor's theorem is a folk theorem, only that some proofs aren't even trivial to formalize. Many other things are trivial to formalize, but they still require filling in a lot of obvious steps. It often wouldn't be practically feasible to prove them with a standard first-order calculus, otherwise proof system languages wouldn't need higher order systems with advanced type theory.

> Cantors theorem usually refers to the existence of uncountable sets, which can be proven by showing that there is no bijection between N and R, but also by showing that there is no bijection between a set and its powerset.

Yes, but I was talking about his diagonal argument, not his powerset argument. That's a different proof from a different paper.

> This is only relevant if you say that the real numbers are "infinte strings of digits", which is not a formal definition and therefore not used in mathematics.

Well, I'm not saying that, but the Coq proof seems to assume it. That was the problem I was talking about.