The formalization of the theory of locally convex vector spaces in Mathlib was launched in 2022, when Moritz Doll and I formalized the two standard definitions. From the very beginning, we intended to use it to start working on the theory of distributions (tempered and classical). I will start by giving an overview of what Mathlib knows about locally convex spaces and outlining some plans for future projects. I will then describe joint work with Luigi Massaci where, starting from the general theory, we defined the space of vector-valued classical distributions, and proved continuity of the differentiation of distributions. A key objective of the talk will be to outline the many design choices in this area of Mathlib, with the hope to help the audience understand the API.