Marijn Heule, Research Assistant Professor
University of Texas at Austin
Progress in satisfiability (SAT) solving has enabled answering long-standing open questions in mathematics completely automatically, resulting in clever though potentially gigantic proofs. We illustrate the success of this approach by presenting the solution of the Boolean Pythagorean triples problem. We also produced and validated a proof of the solution, which has been called the "largest math proof ever."