Marijn Heule
ACL2 Seminar, 9/9/2016

TITLE:

Everything's Bigger in Texas: The Largest Math Proof Ever

ABSTRACT:

The Boolean Pythagorean Triples problem has been a long-standing open
problem in Ramsey Theory: Can the set N = {1, 2, 3, ...} of natural
numbers be partitioned into two parts, such that neither part contains
a triple (a, b, c) with a^2 + b^2 = c^2 ?  A prize for the solution
was offered by Ron Graham decades ago.  We show that such a partition
is possible for the set of integers in [1,7824], but that it is not
possible for the set of integers in [1,M] for any M > 7824.  Of
course, it is completely infeasible to attempt proving this directly
by examining all 2^M possible partitions of [1,M] when M = 7825, for
example.  We solve this problem by using the cube-and-conquer
paradigm, a parallel satisfiability solving method that achieves
linear time speedups on many hard problems.  An important role is
played by dedicated look-ahead heuristics, which allowed us to solve
the problem on a cluster with 800 cores in about two days.  Due to the
general interest in this mathematical problem, our result requires a
formal proof.  Exploiting recent progress in unsatisfiability proof
checking, we produced and verified a clausal proof of the smallest
counterexample, which is almost 200 terabytes in size.  From this we
extracted and made available a compressed certificate of 68 gigabytes,
that allows anyone to reconstruct the proof for checking.  These
techniques show great promise for attacking a variety of challenging
problems arising in combinatorics and computer science.