From c060e50e781e6034e4edec685adbb184310256d7 Mon Sep 17 00:00:00 2001
From: Kenny Lau <kc_kennylau@yahoo.com.hk>
Date: Tue, 25 Aug 2026 16:32:52 +0000
Subject: [PATCH 1/2] feat: add comparator

---
 comparator.json | 14 ++++++++++++++
 lakefile.toml   |  4 ++++
 2 files changed, 18 insertions(+)
 create mode 100644 comparator.json

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"]

From efd7f433153f3e433ec7f57a2f4a5dfe2dd0f3fb Mon Sep 17 00:00:00 2001
From: Kenny Lau <kc_kennylau@yahoo.com.hk>
Date: Wed, 26 Aug 2026 11:05:07 +0000
Subject: [PATCH 2/2] add comparator instructions to README

---
 README.md | 8 ++++++++
 1 file changed, 8 insertions(+)

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.