This illustrated historical talk covers the period from around 1890, when graph theory was still mainly a collection of isolated results, to the 1990s, when it had become part of mainstream mathematics. Among many other topics, it includes material on graph and map colouring, factorisation, trees, graph structure, and graph algorithms. 

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.