The formal-proof tag has no usage guidance.

**35**

votes

**4**answers

2k views

### How much of the ATLAS of finite groups is independently checked and/or computer verified?

In a recent talk Serre made some comments about proofs that rely on the classification of finite simple groups (CFSG) and on the ATLAS of Finite Groups. Namely, he said that a proof that relied on the ...

**12**

votes

**1**answer

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