diff --git a/README.md b/README.md
index 0b05d64..e3b1f53 100644
--- a/README.md
+++ b/README.md
@@ -39,6 +39,14 @@ libraries.
 - [`output/problem.lean`](output/problem.lean) is the formal problem statement.
 - [`output/solution.lean`](output/solution.lean) is the formal solution.
 
+## Verifying with Comparator
+
+This repository can be verified against the formal problem statement with the Lean comparator on a Linux machine. First, follow the instructions in [https://github.com/leanprover/comparator](https://github.com/leanprover/comparator) to install comparator. Then, run the following command:
+
+```
+lake env comparator comparator.json
+```
+
 ## License
 
 This repository uses the MIT License. See [LICENSE](LICENSE) for details.
diff --git a/comparator.json b/comparator.json
new file mode 100644
index 0000000..dc58d00
--- /dev/null
+++ b/comparator.json
@@ -0,0 +1,14 @@
+{
+  "challenge_module": "output.problem",
+  "solution_module": "output.solution",
+  "theorem_names": [
+    "key_formula_one",
+    "key_formula_two"
+  ],
+  "permitted_axioms": [
+    "propext",
+    "Quot.sound",
+    "Classical.choice"
+  ],
+  "enable_nanoda": false
+}
diff --git a/lakefile.toml b/lakefile.toml
index 27f13d7..ccd4381 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -18,3 +18,7 @@ rev = "v4.28.0"
 [[lean_lib]]
 name = "PartitionElliptic"
 globs = ["output.solution"]
+
+[[lean_lib]]
+name = "PartitionEllipticProblem"
+globs = ["output.problem"]