# Tagged Questions

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.

37 views

### How to build C-Corn for Coq from source? [on hold]

Trying to install C-Corn via opam install. The problem is that since two weeks I do not see any progress, I see only Processing: make . I have i7 , 8 GB RAM. Is that normal or has something gone ...
555 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-...
3k 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 ...
1k 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. ...
2k 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,...
621 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$$ ...