10
votes
1answer
451 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. ...
8
votes
1answer
389 views

Proving that a combinatorial sequence has no compact formula

Suppose we have a sequence $a_n$ given by some combinatorial formula, e.g. involving a sum of n terms (like ${n \choose k}^{10}3^{-k}$ etc.). Sometimes it is plausible that there is no compact ...