CMSA New Technologies in Mathematics Seminar: Computer-Aided Mathematics and Satisfiability

CMSA EVENTS

Speaker:

Marijn Heule - Dept. of Computer Science, Carnegie Mellon University

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 a proof 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
our progress on applying SAT solving techniques to the chromatic
number of the plane (Hadwiger-Nelson problem), optimal schemes for
matrix multiplication, and the Collatz conjecture.

https://harvard.zoom.us/j/99651364593?pwd=Q1R0RTMrZ2NZQjg1U1ZOaUYzSE02QT09