Directed Topology


This git repository is created with the goal of obtaining formal proofs in the field of Directed Topology written in the Lean theorem prover language. In particular, our aim is the Van Kampen Theorem concerning Fundamental Categories.

This is the port to Lean 4. A version using Lean 3 already exists in a different repository.


Installing Lean can be done by following the leanprover community website. Our project uses Lean version 4.6.0.

This repository can then be cloned by following the instructions on this page.


Dominique Lawson
Dr. H. Basold, Leiden University
Dr. P. Bruin, Leiden University