The largest mathematical proof to date is 200 terabytes in length and unlikely to be checkable by any human being. Marijn Heule of the University of Texas at Austin and colleagues considered the boolean Pythagorean-triples problem, which asks if a set of natural numbers can be divided into two parts such that no part contains three numbers that could be the lengths of the sides of a right-angled triangle. Even with sophisticated "cube-and-conquer" techniques, it took 800 processor cores about two days to complete the proof. The effort returned the answer "no", but the study also raises fundamental questions about the nature and meaning of computer proofs.