The Science of Brute Force

RECENT PROGRESS IN automated reasoning and super-computing gives rise to a new era of brute force. The game changer is SAT, a disruptive, brute-reasoning technology in industry and science. We illustrate its strength and potential via the proof of the Boolean Pythagorean Triples Problem, a long-standing open problem in Ramsey Theory. This 200TB proof has been constructed completely automatically-paradoxically, in an ingenious way. We welcome these bold new proofs emerging on the horizon, beyond human understanding-both mathematics and industry need them.