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.

Activist Bob Moses argued that mathematical literacy was the next civil rights front line. The 2025 CIME workshop will explore what mathematical literacy might mean and why it still matters for citizenship now and in the future. The workshop’s long-term impact relies on the participation of research mathematicians, mathematics educators, educational researchers, teachers of school mathematics, and policymakers working across different perspectives and roles to foster collaboration that will raise the floor for mathematical literacy for citizenship now and in the future.