Lecture
Solving Mathematical Challenges with Symbolic AI
- Date
- Monday 26 May 2025
- Time
- Address
-
Gorlaeus Building
Einsteinweg 55
2333 CC Leiden - Room
- BW0.29
Progress in symbolic AI has enabled the verification of complex systems and the resolution of long-standing open questions in mathematics. This talk will highlight some successes in computer-aided mathematics, including computing Schur number five, resolving Keller's conjecture, and solving the Empty Hexagon problem. Our approach 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 also discuss some very recent breakthroughs in discrete geometry. The final part of the talk will focus on notorious mathematical challenges for which symbolic AI may be well-suited. In particular, we discuss applying the techniques to the Hadwiger-Nelson problem (chromatic number of the plane), optimal schemes for matrix multiplication, and the Collatz conjecture.
About Marijn Heule
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.