Skip to main content

All Questions

Tagged with
Filter by
Sorted by
Tagged with
33 votes
0 answers
2k 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-...
David Roberts's user avatar
  • 35.5k
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 ...
Nate Eldredge's user avatar
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. ...
Nate Eldredge's user avatar
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 ...
David Roberts's user avatar
  • 35.5k