The Pythagorean triples problem, a long-standing open problem in Ramsey Theory, was recently solved using massive parallel SAT solving. This success was possible due to two breakthroughs in the last five years: the ability to produce verifiable proofs for every SAT solving technique, and the combination of old and new heuristics to partition the problem into millions of equally hard (but much easier) subproblems. This talk presents the major advances in proof technology and SAT heuristics, using the solution of the Pythagorean triples problem as guiding example.