[FOM] Formally verifying "checkers is a draw"

[Bas Spitters]

It would be good to record these examples. E.g. here:
https://en.wikipedia.org/wiki/List_of_long_proofs

The ternary Goldbach conjecture is indeed an interesting example.
http://arxiv.org/abs/1312.7748

It uses primality tests:
http://arxiv.org/abs/1305.3062
and interval computations:
arXiv:1305.3087

There was already a discussion with Helfgott and a number of people in
the formal proofs community.

It looks like the primality tests should be in scope of current methods. E.g:
http://coqprime.gforge.inria.fr/

For the interval computations one would hope to use a cluster like in
the verification of the Kepler conjecture.

Bas

On Fri, Aug 15, 2014 at 1:16 AM, AD Brooke-Taylor
<a.brooke-taylor at bristol.ac.uk> wrote:
>> 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/
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>