Formal methods have long provided rigorous foundations for reasoning about the correctness of hardware and software. More recently, the same techniques have also proven effective in advancing mathematical discovery and proofs. This talk presents successes in applying formal methods, especially SAT technology, to longstanding open problems in mathematics. Highlights include computing Schur number five, resolving Keller’s conjecture, and settling the Empty Hexagon problem. These results often involve gigantic but fully checkable proofs, enabling high confidence in their correctness through independent proof validation. We will also present recent advances in discrete geometry and explore how formal reasoning techniques may help tackle open questions such as the Hadwiger-Nelson problem, optimal matrix multiplication schemes, and the Collatz conjecture.

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.