I will present a collaborative project in which we formalized the construction of Brownian motion in Lean. Lean is an interactive theorem prover, with a large mathematical library called Mathlib. I will give an introduction to Lean and Mathlib, explain why one may want to formalize mathematics, and give a tour of the probability theory part of Mathlib. I will then describe the Brownian motion project, its organization, and some of the formalized results. For that project, we developed the theory of Gaussian measures and implemented a proof of Kolmogorov's extension theorem, as well as a modern version of the Kolmogorov-Chentsov continuity theorem based on Talagrand's chaining technique. Finally, I will discuss the next step of the project: formalizing stochastic integrals.

I will report on recent progress on influential conjectures from the 1970s and 1980s (Berry-Tabor, Bohigas-Giannoni-Schmit), which suggest that the spectral statistics of the Laplace-Beltrami operator on a given compact Riemannian manifold should be described either by a Poisson point process or by a random matrix ensemble, depending on whether the  geodesic flow is integrable or “chaotic”. This talk will straddle aspects of analysis, geometry, probability, number theory and ergodic theory, and should be accessible to a broad audience. The two most recent results presented in this lecture were obtained in collaboration with Laura Monk and with Wooyeon Kim and Matthew Welsh. 

We consider particles following a diffusion process in a multi-well potential and attracted by their barycenter (corresponding to the particle approximation of the Wasserstein flow of a suitable free energy). It is well-known that this process exhibits phase transitions: at high temperature, the mean-field limit has a single stationary solution, the N-particle system converges to equilibrium at a rate independent from N and propagation of chaos is uniform in time. At low temperature, there are several stationary solutions for the non-linear PDE, and the limit of the particle system as N and t go to infinity do not commute. We show that, in the presence of multiple stationary solutions, it is still possible to establish local convergence rates for initial conditions starting in some Wasserstein balls (this is a joint work with Julien Reygner). In terms of metastability for the particle system, we also show that for these initial conditions, the exit time of the empirical distribution from some neighborhood of a stationary solution is exponentially large with N and approximately follows an exponential distribution, and that propagation of chaos holds uniformly over times up to this expected exit time (hence, up to times which are exponentially large with N). Exactly at the critical temperature below which multiple equilibria appear, the situation is somewhat degenerate and we can get uniform in N convergence estimates, but polynomial instead of exponential.