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. 

The universal infinitesimal symmetry of a holomorphic field theory is the Lie algebra of holomorphic vector fields. We introduce the higher-dimensional Virasoro algebra and prove a local, universal, form of the Riemann–Roch theorem using Feynman diagrams. We use the concept of a (Jouanoulou) higher-dimensional chiral algebra as developed recently with Gui and Wang. We will remark on applications to superconformal field theory. This project is joint work with Zhengping Gui.