[FOM] Formally verifying "checkers is a draw"

[AD Brooke-Taylor]

>
> 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.  A very
> high-level summary of the proof is that Fejes Toth reduced the conjecture
> to a large finite computation, which was then carried out.  My expectation
> is that this sort of thing is only going to increase in the future.  It
> won't be just one high-profile project that takes months of computation;
> everybody will be generating theorems whose proofs take days (or more) to
> verify with whatever machines are available.  And naturally, we will be
> more interested in using our CPU-days finding new theorems rather than
> re-verifying last week's theorems.
>

I'd like to draw attention to another timely example of this - yesterday at
the International Congress of Mathematicians, Harald Helfgott spoke about
his proof of the ternary Goldbach conjecture, which states that every odd
number n greater than 6 is expressible as the sum of three primes.  The
proof went by using estimation techniques from analytic number theory to
show that the statement is true for n greater than 10^28, and computer
verification to show it is true for n less than that bound (in fact I get
the impression that the computer verification came first, out to about
10^30).  Moreover, to get the analytic estimates to be precise enough, they
computer-verified the Generalised Riemann Hypothesis for the first _large
number_ (I forget how many, sorry) of zeros.

Anticipating the first question you will ask, I have the impression that
custom computer code was used, and in particular not a formal verification
system.  On the other hand, for the GRH calculation Helfgott made a point
of noting that the calculation gave a rigorous proof - other calculations
of the zeros have previously been done that could have been prone to
rounding errors in computer floating point arithmetic; I guess such
possibilities aren't so important if you're really looking for a
counterexample, or are just convincing yourself that the GRH is probably
true.  The calculation used in this proof by contrast looked at intervals
and so avoided that problem.

Best wishes from Seoul!
Andrew

-- 
Dr Andrew Brooke-Taylor
EPSRC Early Career Fellow
School of Mathematics
University of Bristol
http://www.maths.bris.ac.uk/~maadbt/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140815/42e9c580/attachment-0001.html>