Create README.md

samvang · Apr 4, 2024 · e9c1bd3 · e9c1bd3
1 parent 1ed375b
commit e9c1bd3
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/README.md 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.