From e9c1bd32c73dd662a1f4b34ad420a81b9e346300 Mon Sep 17 00:00:00 2001
From: samvang <59202064+samvang@users.noreply.github.com>
Date: Thu, 4 Apr 2024 12:30:57 +0200
Subject: [PATCH] Create README.md

---
 README.md | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 README.md

diff --git a/README.md b/README.md
new file mode 100644
index 0000000..12cdd15
--- /dev/null
+++ b/README.md
@@ -0,0 +1,9 @@
+# Stone Duality in Lean
+
+The first goal is to prove that the categories of Boolean algebras and of profinite spaces are dually equivalent. A "blueprint" of the proof is available [here](https://samvang.github.io/StoneDualityInLean/blueprint/). 
+
+## Dependencies
+
+* The [Lean](https://lean-lang.org/) programming language and theorem prover
+* [Mathlib](https://github.com/leanprover-community/mathlib4/): a library of formalized mathematics
+* [leanblueprint](https://github.com/PatrickMassot/leanblueprint): LaTeX package for making the blueprint.