# 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