Simons Institute for the Theory of Computing and SLMath Joint Workshop: AI for Mathematics and Theoretical Computer Science

This is an exciting time for mathematics, as new technologies for mathematical reasoning provide novel opportunities for mathematical research, communication, and discovery. Mathlib, a library of formal mathematics, now contains one-and-a-half million lines of code. Important results like the proof of polynomial Freiman-Ruzsa conjecture by Gowers, Green, Manners, and Tao and the exponential improvement to the upper bound on Ramsey's theorem by Campos, Griffiths, Morris, and Sahasrabudhe were formally verified in the Lean proof assistant even before they were accepted to journals. Open problems in combinatorics have been solved with the help of automated reasoning, and AI introduced by Deepmind was deemed to have performed at the level of a silver medalist at the most recent International Mathematical Olympiad.

This workshop will introduce mathematicians and theoretical computer scientists to the technologies that underlie these recent successes, namely, proof assistants, automated reasoning, and machine learning. Talks each morning will survey exciting results in the field, and in the afternoons, we will help participants experiment with the tools to get a sense of what they do. We will also encourage participants to think about how they can use the new technologies in their research.