Quantum Groups are defined as $q$-deformations of the Universal Enveloping Algebra of a Lie Algebra. The study of Quantum Groups have deep connections with many areas in Mathematics and Physics. In this talk, I will focus on Crystal Bases of Quantum Group Representations. Crystal Bases are bases of a representation with properties that let us 'take $q$ to $0$' which gives a combinatorial bare-bone model of the representation. I will go through an example of a crystal base of Braided Exterior Powers of a Quantum Group Representation and relate the combinatorics to that of Binary Matrix Lattices.

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.