The Complementary Program has a limited number of memberships that are open to mathematicians whose interests are not closely related to the core programs; special consideration is given to mathematicians who are partners of an invited member of a core program. 

The minimum spanning tree of 100,000 uniformly random points. Colors encode graph distance from the root, which is red. Black points are those whose removal would disconnect at least 5% of the points from the rest.

This program is devoted to the study of the probabilistic and statistical properties of such networks. Central tools include graphon theory for dense graphs, local weak convergence for sparse graphs, and scaling limits for the critical behavior of graphs or stochastic processes on them. The program is aimed at pure and applied mathematicians interested in network problems.

Extremal combinatorics concerns itself with problems about how large or small a finite collection of objects can be while satisfying certain conditions. Questions of this type arise naturally across mathematics, so this area has close connections and interactions with a broad array of other fields, including number theory, group theory, model theory, probability, statistical physics, optimization, 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.