Directed Topology

Description

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.

Installation

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.

Authors

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

License

See LICENSE.md