All Questions

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

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