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.