[FOM] Formally verifying "checkers is a draw"

[Rempe-Gillen, Lasse]

> Many finite computations might be uninteresting, but it is not hard to
> imagine that there might be many interesting theorems whose proofs reduce
> to a finite computation.  A full proof of the interesting theorem might
> need to include the full verification of P(n) for all n <= 26.  Indeed,
> the Kepler conjecture is basically an example of this phenomenon.  

Harald Helfgott's proof of the Ternary Goldbach Conjecture is precisely of this form: He was able to make some serious improvements to previous results to show that the conjecture holds above some certain large bound (something like 10^30 if memory serves). Then current technology was just about sufficient to deal with the remaining cases, combining computer verifications of the (original) Goldbach conjecture and the Generalized Riemann Hypothesis, together with some additional work.