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."
The enormous size of the proof is not important. In fact a shorter proof would have been preferable. However, the size shows that automated tools combined with super computing facilitate solving bigger problems. Moreover, the proof of 200 terabytes can now be validated using highly trustworthy systems, demonstrating that we can check the correctness of proofs no matter their size.
Bio: Marijn Heule is a Research Assistant Professor at the University of Texas at Austin and received his PhD at Delft University of Technology (2008). His contributions to SAT solving have enabled him and others to solve hard problems in formal verification and mathematics. He has developed award-winning SAT solvers and his preprocessing and proof producing techniques are used in many state-of-the-art solvers.