Questions tagged [coq]
Coq is a formal proof management system, also called an interactive theorem prover. It is used to express mathematical assertions, mechanically check proofs of these assertions, find formal proofs, and extract certified programs.
7 questions
59
votes
8
answers
12k
views
How true are theorems proved by Coq?
Less tongue in cheek, is it known what the relative consistency is for theorems proved with an automatic theorem prover? Of course this depends somewhat on what assumptions one makes with respect to ...
- 35.4k
18
votes
4
answers
4k
views
Proof strength of Calculus of (Inductive) Constructions
This is a follow-on from this question, where I pondered the consistency strength of Coq. This was too broad a question, so here is one more focussed. Rather, two more focussed questions:
I've read ...
- 35.4k
18
votes
2
answers
1k
views
Are we sure the calculus of inductive constructions and ZFC plus countably many inaccessible cardinals are equiconsistent?
This answer says,
IIRC, the calculus of inductive constructions is equi-interpretable with ZFC plus countably many inaccessibles — see Benjamin Werner's "Sets in types, types in sets". (...
- 325
84
votes
3
answers
6k
views
How do I verify the Coq proof of Feit-Thompson?
I probably don't have the appropriate background to even ask this question. I know next to nothing about formal or computer-aided proof, and very little even about group theory. And this question is ...
- 29.7k
20
votes
1
answer
4k
views
Where can I find Gonthier's Coq code proving the four color theorem?
In a 2008 article in the Notices, Georges Gonthier announced a computer-checked proof of the four color theorem using Coq:
Gonthier, Georges. Formal proof—the four-color theorem.
Notices Amer. ...
- 29.7k
2
votes
2
answers
966
views
How to interpret conflicting formal proofs about "a mod 0 = ? "
The proof assistants Coq and Isabelle give conflicting formal proofs about $a \mod 0 \qquad \forall a \in \mathbb{Z}$.
According to Coq
$$ a \mod 0 = 0$$
and Isabelle proves
$$ a \mod = a$$
...
- 25.4k
0
votes
1
answer
431
views
How bad is Coq proving both $T$ and $\lnot T$? [closed]
Question: How bad is Coq proving both $T$ and $\lnot T$? Can it be abused?
Back in 2011 on the coq-club mailing list there was a thread:
Is the Daniel Schepler's inconsistency real?.
In the thread ...
- 25.4k