Please note that the list below only shows forthcoming events, which may not include regular events that have not yet been entered for the forthcoming term. Please see the past events page for a list of all seminar series that the department has on offer.

 

Past events in this series


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, 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.

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.

 

Wed, 12 Nov 2025
11:00
L4

TBA

Trishen Gunaratnam
(Tata Institute for Fundamental Research)