# 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.

**38**

votes

**1**answer

3k views

### On proof-verification using Coq

So i recently learnt that there is now a certain software called ''Coq'' by which one can check the validity of mathematical proofs. My questions are:
Are there limitations on the kinds of proofs ...

**5**

votes

**1**answer

391 views

### Generalizing Big O notation to arbitrary vector spaces

I'm constructing a Coq library for Big-O notation. Naturally, I'd like it to be as general as possible. The Wikipedia page on Big-O notation says
The generalization to functions taking values in ...

**3**

votes

**2**answers

451 views

### formalisation of Bourbaki, General Topology

Is there a formalisation of Bourbaki, General Topology book,
particularly its first chapter?
Are there formal proofs of elementary topology arguments such as a Hausdorff compact space is ...

**26**

votes

**0**answers

938 views

### Next steps on formal proof of classification of finite simple groups

While people are steaming ahead on finessing the proof of the classification of finite simple groups (CFSG), we have a formal proof in Coq of one of the first major components: the Feit-Thompson odd-...

**71**

votes

**3**answers

4k 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 ...

**17**

votes

**1**answer

3k 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. ...

**46**

votes

**3**answers

3k views

### Function extensionality: does it make a difference? why would one keep it out of the axioms?

Yesterday I was shocked to discover that function extensionality (the statement that if two functions $f$ and $g$ on the same domain satisfy $f\left(x\right) = g\left(x\right)$ for all $x$ in the ...

**37**

votes

**35**answers

4k views

### Formalizations of category theory in proof assistants

What are the existing formalizations of category theory in proof assistants?
I'm primarily interested in public-domain code implementing category theory in a proof assistant (Coq, Agda, Isabelle/HOL, ...

**2**

votes

**2**answers

744 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$$
...

**4**

votes

**0**answers

3k views

### Why should I trust Coq when assumption-free proof of False in Coq exists? [closed]

Damien Pous announced code for assumption-free proof of False in Coq which means inconsistency in Coq (without using exploits, lol).
Damien is critical of "fully certified decision procedure ...

**14**

votes

**4**answers

2k 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 ...

**43**

votes

**7**answers

8k 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 ...