Solving Mathematical Challenges with Symbolic AI

Speaker: Marijn Heule, Carnegie Mellon University

Date & Time: Tuesday, 11 March 2025 10:30-12:00 AM

Location: HG-00C29 (Aurora), Hoofdgebouw VU, De Boelelaan 1105, Amsterdam

About the Speaker

Marijn J.H. Heule is a computer scientist specializing in automated reasoning, formal verification, and combinatorial problem-solving using symbolic AI. He is a researcher and professor at Carnegie Mellon University (CMU), known for his work in SAT solving (Boolean Satisfiability) and computer-aided mathematics.

Talk Overview

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 AI-based 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. The final part of the talk will focus on notorious math challenges for which symbolic AI may well be suitable. 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.

Join us for an insightful discussion on the role of symbolic AI in solving mathematical challenges.