Date: Thursday, September 4, 2025
Time: 11:45 a.m. to 12:45 p.m.
Location: G01 Gates Hall
Speaker: Marijn Heule, Associate Professor of Computer Science at Carnegie Mellon University
Abstract:
Automated reasoning has transformed the way we establish trust in complex systems, providing robust guarantees for the correctness of hardware and software. Today, the same techniques are beginning to reshape mathematics. By harnessing the power of automated reasoning, especially SAT solvers, we can now confront challenges that resisted decades of human effort. This talk highlights breakthroughs, including computing Schur Number Five, resolving Keller’s conjecture, and settling the Empty Hexagon problem. Each achievement produced a massive yet independently verifiable proof, offering high confidence in its correctness. We will also cover recent advances in discrete geometry and discuss some long-standing open challenges, including the Hadwiger-Nelson problem and the Collatz conjecture. These developments point to a new era in which human insight and automated reasoning collaborate to expand the boundaries of mathematical knowledge.
Bio:
Marijn Heule is an Associate Professor of Computer Science at Carnegie Mellon University. His contributions to automated reasoning have enabled him and others to solve hard problems in formal verification and mathematics. He has developed award-winning satisfiability (SAT) solvers. His preprocessing and proof-producing techniques are used in many state-of-the-art automated reasoning tools. Marijn won multiple best paper awards at international conferences, including at SAT, CADE, IJCAR, TACAS, HVC, LPAR, and IJCAI-JAIR. He is one of the editors of the Handbook of Satisfiability. This 1500+ page handbook (second edition) has become the reference for SAT research.
