[lmm]

> It follows from this that it must exist some statements that are undecidable in Coq, correct?

Yes, but only those that are undecidable in ordinary mathematics. If you're not using Coq, you have exactly the same problem. (And this concern doesn't apply if we already have the proof and just want to check it).

[ngrilly]

> Yes, but only those that are undecidable in ordinary mathematics. If you're not using Coq, you have exactly the same problem.

Yes, this is what I understood. Thanks for confirming this point.

> (And this concern doesn't apply if we already have the proof and just want to check it).

Why this concern would not apply anymore if we already have the proof and just want to check it? The proof still needs to be expressed, directly or indirectly, in terms of Zermelo–Fraenkel set theory combined with first-order logic. If the proof uses a different and "incompatible" theory, how could we check it with Coq?

(I understand this is a very rare occurence in practice and this is the reason why ZFC is so much used.)

[lmm]

> The proof still needs to be expressed, directly or indirectly, in terms of Zermelo–Fraenkel set theory combined with first-order logic. If the proof uses a different and "incompatible" theory, how could we check it with Coq?

If Wiles' proof wasn't in ZFC we wouldn't call it a proof (at least not without qualification). You don't get to just write mathematical proofs in any language you like - otherwise we could pick a language in which FLT is an axiom, and then the proof of it is trivial.

[ngrilly]

I don't get it. There is a lot of variants of set theory. ZFC is just one of them, albeit the most common. But some proofs are founded on an extension of ZFC. For example, the Mizar system, which is another proof assistant, has adopted Tarski–Grothendieck set theory, an extension of ZFC.

According to "The QED Manifesto Revisited" [1], it can be difficult to use Coq as-is for some kind of proofs:

> Here are four mathematical statements that most mathematicians will consider to be totally non-problematic: [...] We claim that currently none of the QED-like systems can express all four statements in a good way. Of course one can easily extend the systems with axioms that allow one to write down these statements. However, that really amounts to ‘changing the system’. It would mean that both the library and the automation of the system will not be very useful anymore. Classical & extensional reasoning in Coq or abstract algebra in the HOLs by postulating the necessary types and axioms will not be pleasant without re-engineering the system.

[1] http://mizar.org/trybulec65/8.pdf

[lmm]

> I don't get it. There is a lot of variants of set theory. ZFC is just one of them, albeit the most common. But some proofs are founded on an extension of ZFC. For example, the Mizar system, which is another proof assistant, has adopted Tarski–Grothendieck set theory, an extension of ZFC.

Some mathematicians accept extensions of ZFC. But I would definitely expect a proof that relied on such an extension to have in big red letters "we use these additional axioms", and the mathematical community would hope for and expect a proof without it. (Indeed proofs that make use of the axiom of choice still often flag this up and we look for proofs without it where possible). I am quite surprised that Mizar would do this, and certainly hope that it provides a way to distinguish between proofs that are valid in ZFC and those that aren't.

> According to "The QED Manifesto Revisited" [1], it can be difficult to use Coq as-is for some kind of proofs:

The statement about aleph-0 and aleph-2 (the one that Coq has problems with) isn't really mathematics so much as metamathematics/proof theory, at least if we're viewing it as a statement about the consequences of axioms. Which sure is a valuable field and one we'd like to be able to reason about, but it's circumscribed and doesn't affect normal working mathematics.

If we're talking about accepting that axiom and actually using it in a proof, then it's certainly not "totally non-problematic". The paper admits that most mathematicians wouldn't even know the statement of the proper forcing axiom. They certainly wouldn't write proofs that depended on it.

[ngrilly]

Thanks a lot @lmm. Now I get it :)

About Mizar, I don't know if you can use it without the additional axioms of Tarski-Grothendieck set theory.