feat: add comparator

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.

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
+}

lakefile.toml

@@ -18,3 +18,7 @@ rev = "v4.28.0"
 [[lean_lib]]
 name = "PartitionElliptic"
 globs = ["output.solution"]
+
+[[lean_lib]]
+name = "PartitionEllipticProblem"
+globs = ["output.problem"]