From 2063771a7308ebb5e76b27f22921377988bcf762 Mon Sep 17 00:00:00 2001
From: Kenny Lau <kc_kennylau@yahoo.com.hk>
Date: Wed, 26 Aug 2026 11:53:20 +0000
Subject: [PATCH] feat: add comparator

---
 README.md       |  8 ++++++++
 comparator.json | 15 +++++++++++++++
 lakefile.toml   |  4 ++++
 3 files changed, 27 insertions(+)
 create mode 100644 comparator.json

diff --git a/README.md b/README.md
index b45d722..cc6bcf3 100644
--- a/README.md
+++ b/README.md
@@ -36,6 +36,14 @@ libraries.
 - [`problem.lean`](output/problem.lean) is the formal problem statement.
 - [`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..0581ca4
--- /dev/null
+++ b/comparator.json
@@ -0,0 +1,15 @@
+{
+  "challenge_module": "output.problem",
+  "solution_module": "output.solution",
+  "theorem_names": [
+    "thm_main",
+    "lem_proximity",
+    "cor_density"
+  ],
+  "permitted_axioms": [
+    "propext",
+    "Quot.sound",
+    "Classical.choice"
+  ],
+  "enable_nanoda": false
+}
diff --git a/lakefile.toml b/lakefile.toml
index 783e9de..ede9ff1 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -18,3 +18,7 @@ rev = "v4.28.0"
 [[lean_lib]]
 name = "TanArctan"
 globs = ["output.solution"]
+
+[[lean_lib]]
+name = "TanArctanProblem"
+globs = ["output.problem"]