Return to Answer

Here are some publications related to your question:

• Robert Pollack. How to believe a machine-checked proof. In G. Sambin and J. Smith, editors, Twenty Five Years of Constructive Type Theory. Oxford Univ. Press, 1998. doi:10.1093/oso/9780198501275.003.0013, (also freely available as BRICS Report Series, 4(18) (1997) doi:10.7146/brics.v4i18.18945) (Wayback Machine of author's gzipped ps file)

In Pollack-inconsistency (published in Electronic Notes in Theoretical Computer Science), Freek Wiedijk demonstrates the most popular proof assistants are Pollack inconsistent.

In an internet post Pollack discusses Coq coercions:

The problem is that Coq coercions are informally specified and behave somewhat unpredictably. A formal theory of coercions, such as Luo's Coercive subtyping (with proof theory and semantics) would eliminate this question of the meaning of statements using coercions. However, the proof theory of coercions is complicated.

Here are some publications related to your question:

• Robert Pollack. How to believe a machine-checked proof. In G. Sambin and J. Smith, editors, Twenty Five Years of Constructive Type Theory. Oxford Univ. Press, 1998. doi:10.1093/oso/9780198501275.003.0013, (also freely available as BRICS Report Series, 4(18) (1997) doi:10.7146/brics.v4i18.18945) (Wayback Machine of author's gzipped ps file)

In Pollack-inconsistency (published in Electronic Notes in Theoretical Computer Science), Freek Wiedijk demonstrates the most popular proof assistants are Pollack inconsistent.

In an internet post Pollack discusses Coq coercions:

The problem is that Coq coercions are informally specified and behave somewhat unpredictably. A formal theory of coercions, such as Luo's Coercive subtyping (with proof theory and semantics) would eliminate this question of the meaning of statements using coercions. However, the proof theory of coercions is complicated.

Added later

The consistency and expressive power of Coq depend on time and bugs fixed vs bugs introduces.

Some versions of Coq fail to prove provable theorems, e.g. check How do I verify the Coq proof of Feit-Thompson?

The error you get is a real one, but is not in the proof of the odd order theorem. It is in Coq. Let me be more clear: a bug in the kernel of Coq

Inconsistency bugs appear more common, Preliminary compilation of critical bugs in stable releases of Coq. In around 2008 I reported inconsistency bug and to my surprise Coq devs called the proof of concept code exploit.

Here are some publications related to your question:

Robert Pollack. How to believe a machine-checked proof. In G. Sambin and J. Smith, editors, Twenty Five Years of Constructive Type Theory. Oxford Univ. Press, 1998. (Wayback Machine)

Pollack-inconsistency, Freek Wiedijk Freek demonstrates the most popular proof assistants are Pollack inconsistent.

In an internet post Pollack discusses Coq coercions:

The problem is that Coq coercions are informally specified and behave somewhat unpredictably. A formal theory of coercions, such as Luo's Coercive subtyping (with proof theory and semantics) would eliminate this question of the meaning of statements using coercions. However, the proof theory of coercions is complicated.

Here are some publications related to your question:

• Robert Pollack. How to believe a machine-checked proof. In G. Sambin and J. Smith, editors, Twenty Five Years of Constructive Type Theory. Oxford Univ. Press, 1998. doi:10.1093/oso/9780198501275.003.0013, (also freely available as BRICS Report Series, 4(18) (1997) doi:10.7146/brics.v4i18.18945) (Wayback Machine of author's gzipped ps file)

In Pollack-inconsistency (published in Electronic Notes in Theoretical Computer Science), Freek Wiedijk demonstrates the most popular proof assistants are Pollack inconsistent.

In an internet post Pollack discusses Coq coercions:

The problem is that Coq coercions are informally specified and behave somewhat unpredictably. A formal theory of coercions, such as Luo's Coercive subtyping (with proof theory and semantics) would eliminate this question of the meaning of statements using coercions. However, the proof theory of coercions is complicated.

Here are some publications related to your question:

Robert Pollack. How to believe a machine-checked proof. In G. Sambin and J. Smith, editors, Twenty Five Years of Constructive Type Theory. Oxford Univ. Press, 1998.

Pollack-inconsistency, Freek Wiedijk Freek demonstrates the most popular proof assistants are Pollack inconsistent.

In an internet post Pollack discusses Coq coercions:

The problem is that Coq coercions are informally specified and behave somewhat unpredictably. A formal theory of coercions, such as Luo's Coercive subtyping (with proof theory and semantics) would eliminate this question of the meaning of statements using coercions. However, the proof theory of coercions is complicated.

Here are some publications related to your question:

Robert Pollack. How to believe a machine-checked proof. In G. Sambin and J. Smith, editors, Twenty Five Years of Constructive Type Theory. Oxford Univ. Press, 1998. (Wayback Machine)

Pollack-inconsistency, Freek Wiedijk Freek demonstrates the most popular proof assistants are Pollack inconsistent.

In an internet post Pollack discusses Coq coercions:

The problem is that Coq coercions are informally specified and behave somewhat unpredictably. A formal theory of coercions, such as Luo's Coercive subtyping (with proof theory and semantics) would eliminate this question of the meaning of statements using coercions. However, the proof theory of coercions is complicated.