What do you mean by "transfinite proofs"? Let's look at Cantor's proof. It is: For every set A and function f : A -> P(A) there exists y in P(A) such that for

What do you mean by "transfinite proofs"? Let's look at Cantor's proof. It is: For every set A and function f : A -> P(A) there exists y in P(A) such that for all x, f(x) /= y. Proof: Define y = {a: a is not in f(a)}. If f(x) = y, then f(x) = {a: a is not in f(a)}, but this implies x is in f(x) <=> x is not in f(x), contradiction. It does not mention infinity anywhere! It only says that there cannot be a surjection between one set and the other. We could call this situation "transfinite" but this is only a name; under the hood, this is a normal proof of properties of functions, using very natural reasoning rules. That's why I disagreed - there's nothing special in Cantor's proof from a formal viewpoint, possible concerns are of psychological/historical nature, which are not relevant to a machine. It is true that changing foundations might require rewriting the prover. However, humans also need time to adjust to a new formal system. For example, it takes a lot of effort to get a good grasp of intuitionistic logic. This might be a concern, but ZFC is a very well-grounded common framework for mathematicians, and this is extremely unlikely to change. Perhaps calculus of constructions, as a version of lambda calculus, is closer to computation, and this is why it was chosen in Coq. I'm not sure. Mizar (another theorem-proving environment) is based on an extension of ZFC. [ZFC is untyped - everything is a set, while CoC has a rich type system.] Small nitpick: It's not like proofs involving unique choice + excluded middle cannot be expressed in Coq; they can, but as the system is inconsistent, they have no value, as everything is provable.