 After splitting the problem into 106 hard subproblems (known as “cubes”), these were handed down to 800 cores working in parallel on a Stampede supercomputer which, after 2 days of further splitting and CDCL clause-crunching, settled the question and delivered a 200-terabyte proof validating the work. After deservedly celebrating this significant accomplishment of automated reasoning, and after entertaining all the new applications that the enhanced SAT method would afford (particularly in the areas of hardware and software verification), we should then ask some questions that are of especial importance to mathematicians: Is there a more insightful way to establish this result that would involve more traditional and intellectually satisfying mathematical proof methods? Or, as far as increasing our understanding of a given field (combinatorics in this case), what is the value of settling a question when no human can inspect the proof and hence get no insight from it? Even the team responsible for the result admits that “the proofs of unsatisfiability coming from SAT solvers are, from a human point of view, a giant heap of random information (no direct understanding is involved)”. The conjecture has been settled but we basically have no underlying idea what makes 7825 so special. Perhaps the real value to be drawn from these considerations is that they lead us to think about the deeper question: What is it about the structure of a specific problem that makes it amenable to standard mathematical treatment as opposed to requiring a mindless brute-force approach? While this question is being contemplated, SAT may provide the best line of attack on certain mathematical problems.