Speaker: Marijn Heule, Carnegie Mellon University

Title: Computer-aided Mathematics: Successes, Advances, and Trust

Day: Tuesday, March 21, 2023

Time: 4:30 PM

Location: B205 Engineering Quadrangle

Host: Sharad Malik

Abstract: Progress in satisfiability (SAT) solving has made it possible to determine the correctness of complex systems and answer long-standing open questions in mathematics. The SAT-solving approach is completely automatic and can produce clever though potentially gigantic proofs.

We can have confidence in the correctness of the answers because highly trustworthy systems can validate the underlying proofs regardless of their size.

We demonstrate the effectiveness of the SAT approach by presenting some recent successes, including the solution of the Boolean Pythagorean Triples problem, computing the fifth Schur number, and resolving the remaining case of Keller’s conjecture. Moreover, we constructed and validated proofs for each of these results. The second part of the talk focuses on notorious math challenges for which automated reasoning may well be suitable. In particular, we discuss advances in applying SAT-solving techniques to the Hadwiger-Nelson problem (chromatic number of the plane), optimal schemes for matrix multiplication, and the Collatz conjecture.

Bio: I am an Associate Professor in the Computer Science Department at Carnegie Mellon University and received my PhD at Delft University of Technology in the Netherlands. My research focuses on solving hard-combinatorial problems in areas such as formal verification, number theory, and extremal combinatorics. Most of my contributions are related to theory and practice of satisfiability (SAT) solving. I have developed award-winning SAT solvers, and my preprocessing techniques are used in state-of-the-art SAT solvers.