The tag has no wiki summary.

learn more… | top users | synonyms

48
votes
3answers
2k 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 ...
10
votes
1answer
532 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. ...
19
votes
32answers
1k 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, ...
1
vote
2answers
481 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$$ ...
2
votes
0answers
1k 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 ...
10
votes
4answers
1k 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 ...