  Directed topology is an area of mathematics with applications in concurrency.
It extends the concept of a topological space by adding a notion of
directedness, which restricts how paths can evolve through a space and enables
thereby a faithful representation of computation with their direction. In this
paper, we present a Lean formalisation of directed spaces and a Van Kampen
theorem for them. This theorem allows the calculation of the homotopy type of a
space by combining local knowledge the homotopy type of subspaces. With this
theorem, the reasoning about spaces can be reduced to subspaces and, by
representing concurrent systems as directed spaces, we can reduce the deduction
of properties of a composed system to that of subsystems. The formalisation in
Lean can serve to support computer-assisted reasoning about the behaviour of
concurrent systems.
