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 over two 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 prove 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 hybrid SAT method for hard problems, employing both look-ahead and CDCL solvers. An important role is played by dedicated look-ahead heuristics, which indeed allowed us to solve the problem on a cluster with 800 cores in about 2 days. Due to the general interest in this mathematical problem, our result requires a formal proof. Exploiting recent progress in unsatisfiability proofs of SAT solvers, we produced and verified a proof in the DRAT format, 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 DRAT proof for checking. These techniques show great promise for attacking a variety of similar computational problems arising in combinatorics and computer science.