diff --git a/README.md b/README.md
new file mode 100644
index 0000000..16b7ad8
--- /dev/null
+++ b/README.md
@@ -0,0 +1,18 @@
+About Minesweeper.Reasoning
+===========================
+
+Minesweeper.Reasoning is an Agda module providing a formal description of the game
+[Minesweeper](https://en.wikipedia.org/wiki/Minesweeper_(video_game)) and proofs about it, inspired by
+[ProofSweeper](https://github.com/A1kmm/proofsweeper/). In ProofSweeper, you play Minesweeper by formally proving in Idris that
+cells are or aren't mines, using some provided axioms, rather than simply clicking to uncover them.
+My goal with Minesweeper.Reasoning is to prove that those axioms are sound (if you use them to prove that a cell is or isn't
+a mine, that will always be the case) and complete (if a cell is always or never a mine, you can prove it with those axioms).
+
+These proofs are found in `Minesweeper/Reasoning.agda`. The formalization of Minesweeper is split across the remaining modules;
+of note, `Minesweeper/Rules.agda` and `Minesweeper/Moves.agda` contain the main definitions, along with some useful lemmas.
+
+Dependencies
+============
+
+Minesweeper.Reasoning was checked against [Agda v2.6.0.1](https://github.com/agda/agda/releases/tag/v2.6.0.1)
+and requires [agda-stdlib v1.1](https://github.com/agda/agda-stdlib/releases/tag/v1.1).