This tutorial will be a hands-on introduction to proving theorems in Lean, using its mathematical library Mathlib. It will not assume any previous knowledge about formal theorem provers. We will discover the Lean language, learn how to read a statement and a proof, and learn the essential "tactics" one can use to prove theorems in Lean.

Participants should come with a computer, and it would be best if they could install Lean before the tutorial by following the instructions at https://lean-lang.org/install/ . The installation should be easy and takes only a few minutes.

Given a finite poset $P$ we ask how small a family of subsets of $[n]$ can be such that it does not contain an induced copy of the poset, but adding any other subset creates such a copy. This number is called the saturation number of $P$, denoted by $\operatorname{sat}^*(n,P)$. Despite the apparent similarity to the saturation for graphs, this notion is vastly different. For example, it has been shown that the saturation numbers exhibit a dichotomy: for any poset, the saturation number is either bounded, or at least $2 n^{1/2}$. In fact, it is believed that the saturation number is always bounded or exactly linear. In this talk we will be discussing the most recent advances in this field, with the focus on the diamond poset, whose saturation number was unknown until recently.

Joint with Sean Jaffe.

We consider targeted intervention problems in dynamic network and graphon games. First, we study a general dynamic network game in which players interact over a graph and seek to maximize their heterogeneous, concave goal functionals. We establish the existence and uniqueness of a Nash equilibrium in both the finite-player network game and the corresponding infinite-player graphon game, and prove its convergence as the number of players tends to infinity. We then introduce a central planner who implements a dynamic targeted intervention. Given a fixed budget, the central planner maximizes the average welfare at equilibrium by perturbing the players' heterogeneous goal functionals. Using a novel fixed-point argument, we prove the existence and uniqueness of an optimal intervention in the graphon setting, and show that it achieves near-optimal performance in large finite networks. Finally, we study the special case of linear-quadratic goal functionals and derive semi-explicit solutions for the optimal intervention.

 

This is a joint work with Sturmius Tuschmann.  

Just as parallel threebranes on a smooth manifold are related to string theory on AdS_5 \times S^5, parallel threebranes near a conical singularity are related to string theory on AdS_5 \times X_5 for a suitable X_5. For the example of the conifold singularity Klebanov and Witten conjectured that a string theory on AdS_5 \times X^5 can be described by a certain \mathcal{N}=1 supersymmetric gauge theory. Based primarily on their work (arXiv:hep-th/9807080), I describe the gravitational setup of this correspondence as well as their construction of the field theory, allowing for various checks of the duality.

Junior Strings is a seminar series where DPhil students present topics of common interest that do not necessarily overlap with their own research area. This is primarily aimed at PhD students and post-docs but everyone is welcome.

TBC