Thu, 30 Oct 2025

12:00 - 13:00
C5

Differentiation on metric spaces

Pietro Wald
(University of Warwick)
Abstract
Cheeger’s seminal 1999 paper initiated the study of metric measure spaces that admit a generalised differentiable structure. In such spaces, Lipschitz functions—real-valued and, in some cases, Banach-valued—are differentiable almost everywhere. Since then, much work has gone into determining the precise geometric and analytic conditions under which such structures exist. In this talk, I will give a brief overview of the theory and present new results from joint work with David Bate.
Wed, 12 Nov 2025
11:00
L4

TBA

Trishen Gunaratnam
(Tata Institute for Fundamental Research)
Wed, 05 Nov 2025
11:00
L4

Coming up from $-\infty$ for KPZ via stochastic control

Carlos Villanueva Mariz
(Free University Berlin)
Abstract

We derive a lower bound, independent of the initial condition, for the solution of the KPZ equation on the torus, using its representation as the value function of a stochastic control problem.

With the same techniques we also prove a bound for its oscillation, again independent of initial conditions, which is related to Harnack's inequality for the (rough) heat equation.

 

Tue, 04 Nov 2025
13:45
L3

Lean tutorial (part 2)

Remy Degenne
(INRIA LILLE)
Abstract

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.

Tue, 04 Nov 2025
12:00
L4

Lean tutorial (part 1)

Remy Degenne
(INRIA LILLE)
Abstract
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.
Tue, 25 Nov 2025

14:00 - 15:00
L4

TBA

Maria-Romina Ivan
(University of Cambridge, Stanford University)
Fri, 24 Oct 2025
11:00
L3

Higher-Form Anomalies on Lattice

Ryohei Kobayashi
(IAS Princeton)
Abstract
Higher-form symmetry in a tensor product Hilbert space is always emergent: the symmetry generators become genuinely topological only when the Gauss law is energetically enforced at low energies. In this talk, I explain a general method for defining the 't Hooft anomaly of higher-form symmetries in lattice models built on a tensor product Hilbert space. For instance, this allows us to define an index valued in $H^4(B^2G, U(1))$ characterizing the ’t Hooft anomaly of 1-form symmetry (2+1)D, for given finite depth circuits generating the symmetry. I also outline a criteria for “onsiteability” of higher-form symmetry based on an ongoing work with collaborators.


 

Short stories 1

When you next go swimming, take some maths with you. And don't worry, maths is waterproof. Nathan Creighton is in at the deep end.

Subscribe to