From c1cfb817263644a432795d06ee3ae22d939c15e2 Mon Sep 17 00:00:00 2001 From: userName Date: Fri, 24 Apr 2026 11:54:05 +0800 Subject: [PATCH 1/2] Add evaluation datasets --- .gitattributes | 1 + data/Prop_name.txt | 100 +++++++++++++++++++++++++ data/README.md | 84 +++++++++++++++++++++ data/expressions.txt | 100 +++++++++++++++++++++++++ data/test_set_B_tactic_step.sql.tar.gz | 3 + 5 files changed, 288 insertions(+) create mode 100644 data/Prop_name.txt create mode 100644 data/README.md create mode 100644 data/expressions.txt create mode 100644 data/test_set_B_tactic_step.sql.tar.gz diff --git a/.gitattributes b/.gitattributes index e247b81..cc4e3ab 100644 --- a/.gitattributes +++ b/.gitattributes @@ -1 +1,2 @@ data/*.sql.xz filter=lfs diff=lfs merge=lfs -text +data/*.sql.tar.gz filter=lfs diff=lfs merge=lfs -text diff --git a/data/Prop_name.txt b/data/Prop_name.txt new file mode 100644 index 0000000..12e05c4 --- /dev/null +++ b/data/Prop_name.txt @@ -0,0 +1,100 @@ +Nat.add_comm +Nat.lt_asymm +Nat.div_eq_sub_div +Nat.gcd_mul_left +Fin.val_add_one_le_of_lt +Nat.mul_div_left +Nat.add_div_right +Nat.div_eq_of_lt_le +Nat.mul_div_le +Nat.exists_eq_add_of_le +Nat.add_one_le_add_one_iff +Nat.div_eq_of_lt_le +Nat.nextPowerOfTwo_dec +Nat.add_lt_add_of_le_of_lt +Nat.add_sub_cancel_right +Nat.sub_le_iff_le_add +Nat.mul_left_cancel +Nat.mul_lt_mul_of_lt_of_le +Nat.pow_lt_pow_of_lt +Nat.dvd_gcd +Nat.add_left_comm +Nat.add_right_comm +Nat.add_left_cancel +Nat.add_right_cancel +Nat.eq_zero_of_add_eq_zero +Nat.eq_zero_of_add_eq_zero_left +Nat.mul_zero +Nat.mul_succ +Nat.mul_add_one +Nat.zero_mul +Nat.succ_mul +Fin.ne_of_val_ne +Fin.val_ne_of_ne +Fin.modn_lt +Fin.val_lt_of_le +Fin.pos +Fin.ne_of_val_ne +Fin.val_inj +Fin.val_congr +Fin.val_le_of_le +Fin.val_le_of_ge +Fin.val_add_one_le_of_lt +Fin.val_add_one_le_of_gt +Fin.exists_iff +Nat.exists_ne_zero +Nat.exists_eq_add_one +Nat.exists_add_one_eq +Nat.forall_lt_succ_right' +Nat.forall_lt_succ_right +Nat.forall_lt_succ_left' +Nat.forall_lt_succ_left +Nat.exists_lt_succ_right' +Nat.exists_lt_succ_right +Nat.exists_lt_succ_left' +Nat.exists_lt_succ_left +Nat.add_add_add_comm +Nat.one_add +Nat.succ_eq_one_add +Nat.succ_add_eq_add_succ +Nat.eq_zero_of_add_eq_zero_right +Nat.add_eq_zero_iff +Nat.add_left_cancel_iff +Nat.add_right_cancel_iff +Nat.add_left_eq_self +Nat.add_right_eq_self +Nat.self_eq_add_right +Nat.self_eq_add_left +Nat.add_le_add_iff_left +Nat.lt_of_add_lt_add_right +Nat.lt_of_add_lt_add_left +Nat.add_lt_add_iff_left +Nat.add_lt_add_iff_right +Nat.add_lt_add_of_le_of_lt +Nat.add_lt_add_of_lt_of_le +Nat.pos_of_lt_add_right +Nat.pos_of_lt_add_left +Nat.lt_add_right_iff_pos +Nat.lt_add_left_iff_pos +Nat.add_pos_left +Nat.add_pos_right +Nat.add_self_ne_one +Nat.sub_one +Nat.one_sub +Nat.succ_sub_sub_succ +Nat.add_sub_sub_add_right +Nat.sub_right_comm +Nat.add_sub_cancel_right +Nat.add_sub_cancel' +Nat.succ_sub_one +Nat.one_add_sub_one +Nat.sub_sub_self +Nat.sub_add_comm +Nat.sub_eq_zero_iff_le +Nat.sub_pos_iff_lt +Nat.sub_le_iff_le_add +Nat.sub_le_iff_le_add' +Nat.le_sub_iff_add_le +Int.lcm_ne_zero +Int.dvd_lcm_left +Int.dvd_lcm_right \ No newline at end of file diff --git a/data/README.md b/data/README.md new file mode 100644 index 0000000..554b59c --- /dev/null +++ b/data/README.md @@ -0,0 +1,84 @@ +\# Data + + + +This directory contains the database dumps and test sets used in this repository. + + + +\## Files + + + +\- `mathlib\_filtered\_backup0515.sql.xz` + + PostgreSQL dump of the `mathlib\_filtered` table. This table contains the filtered Mathlib theorem corpus used as the retrieval candidate library. + + + +\- `wl\_encodings\_new\_backup0515.sql.xz` + + PostgreSQL dump of the precomputed WL/tree encodings used by the retrieval pipeline. + + + +\- `expressions.txt` + + Query expressions for Test Set A. Each line is one Lean-style query expression. + + + +\- `Prop\_name.txt` + + Ground-truth theorem names for Test Set A. Line `i` corresponds to line `i` in `expressions.txt`. + + + +\- `test\_set\_B\_tactic\_step.sql.tar.gz` + + Compressed PostgreSQL backup for Test Set B. It contains proof-step records used to reconstruct the evaluation examples. + + + +\## Test Set A + + + +Test Set A is a small manually constructed benchmark for premise selection. + + + +It consists of two line-aligned files: + + + +```text + +expressions.txt + +Prop\_name.txt + + + +The correspondence is: + + + +expressions.txt line i -> query expression + +Prop\_name.txt line i -> target theorem name + +Test Set B + + + +Test Set B is provided as a compressed PostgreSQL backup: + + + +test\_set\_B\_tactic\_step.sql.tar.gz + + + +It is built from proof-step records extracted from Lean proof traces. + diff --git a/data/expressions.txt b/data/expressions.txt new file mode 100644 index 0000000..d6e7e3e --- /dev/null +++ b/data/expressions.txt @@ -0,0 +1,100 @@ +q((n m : Nat) → (n + 1) + m = m + (n + 1)) +q({a b c : Nat} → (h : a + c < b) → ¬ b < a + c) +q({b a : Nat} → (h₁ : 0 < b) → (h₂ : b ≤ a.succ) → a.succ / b = (a.succ - b) / b + 1) +q((m n k : Nat) → (m.succ * n).gcd (m.succ * k) = m.succ * n.gcd k) +q({n : Nat} → {a b : Fin n.succ} → (h : a < b) → ↑a + 1 ≤ ↑b) +q((m : Nat) → {n : Nat} → (H : 0 < n.pred) → m * n.pred / n.pred = m) +q((x : Nat) → {z₁ z₂ : Nat} → (H : 0 < z₁ + z₂) → (x + (z₁ + z₂)) / (z₁ + z₂) = x / (z₁ + z₂) + 1) +q({k n m : Nat}→ (lo : k.pred * n.succ ≤ m) → (hi : m < (k.pred + 1) * n.succ) → m / n.succ = k.pred) +q((m n r : Nat) → n * ((m + r) / n) ≤ m + r) +q({m n : Nat} → (h : m ≤ n.succ) → ∃ k, n.succ = m + k) +q({a b : Nat} → a + 2 ≤ b + 2 ↔ a ≤ b) +q({k n m : Nat} → (hi : m < (k + 1) * n) → (lo : k * n ≤ m) → m / n = k) +q({n power : Nat} → (h₂ : power < n) → (h₁ : power > 0) → n - power * 2 < n - power) +q({a b c d : Nat} → (hlt : c < d) → (hle : a ≤ b) → a + c < b + d) +q((n m : Nat) → n = n + m - m) +q({a b c : Nat} → a ≤ c + b ↔ a - b ≤ c) +q({n m k : Nat} → (h : n * m.succ = n * k) → (np : 0 < n) → m.succ = k) +q({a c b d : Nat} → (hbd : b ≤ d.succ) → (hac : a < c) → (hd : 0 < d.succ) → a * b < c * d.succ) +q({a n m : Nat} → (w : n < m) → (h : 1 < a.pred) → a.pred ^ n < a.pred ^ m) +q({k m n : Nat} → k.succ ∣ m → k.succ ∣ n → k.succ ∣ m.gcd n) +q((b c : Nat) → 1 + (b + c) = b + (1 + c)) +q((n b c : Nat) → (n + b) + c = (n + c) + b) +q({a b : Nat} → a + b = a + 1 → b = 1) +q({a b : Nat} → a + (b + 1) = (b + 1) + a → a = b) +q({a : Nat} → a + 0 = 0 → a = 0) +q({a n: Nat} → a + (n + 1) = 0 → (n + 1) = 0) +q((b : Nat) → b * 0 = 0) +q((a n : Nat) → a * (n + 1).succ = a * (n + 1) + a) +q((a : Nat) → a * (1 + 1) = a * 1 + a) +q((a : Nat) → 0 * 0 = 0) +q((n m : Nat) → (n + 1).succ * m = (n + 1) * m + m) +q((n : Nat) → (i j : Fin n) → i.val ≠ j.val → i ≠ j) +q((n : Nat) → (i j : Fin n) → i ≠ j → i.val ≠ j.val) +q({n m : Nat} → (i : Fin n) → m > 0 → (Fin.modn i m).val < m) +q((b n : Nat) → (i : Fin b) → b ≤ n → i.val < n) +q((n : Nat) → (i : Fin n) → 0 < n) +q((n : Nat) → (i j : Fin n) → i.val ≠ j.val → i ≠ j) +q((n : Nat) → {a b : Fin n} → a.1 = b.1 ↔ a = b) +q({n : Nat} → {a b : Fin n} → a = b → (a : Nat) = (b : Nat)) +q({n : Nat} → {a b : Fin n} → a ≤ b → (a : Nat) ≤ (b : Nat)) +q({n : Nat} → {a b : Fin n} → a ≥ b → (b : Nat) ≤ (a : Nat)) +q({n : Nat} → {a b : Fin n} → a < b → (a : Nat) + 1 ≤ (b : Nat)) +q({n : Nat} → {a b : Fin n} → a > b → (b : Nat) + 1 ≤ (a : Nat)) +q((n : Nat) → {p : Fin n → Prop} → (∃ i, p i) ↔ ∃ i, ∃ h, p ⟨i, h⟩) +q((P : Nat → Prop) → (∃ n, ¬ n = 0 ∧ P n) ↔ ∃ n, P (n + 1)) +q((a : Nat) → (∃ n, a = n + 1) ↔ 0 < a) +q((a : Nat) → (∃ n, n + 1 = a) ↔ 0 < a) +q((n : Nat) → (p : (m : Nat) → (m < n + 1) → Prop) → (∀ m (h : m < n + 1), p m h) ↔ (∀ m (h : m < n), p m (by omega)) ∧ p n (by omega)) +q((n : Nat) → (p : Nat → Prop) → (∀ m, m < n + 1 → p m) ↔ (∀ m, m < n → p m) ∧ p n) +q((n : Nat) → (p : (m : Nat) → (m < n + 1) → Prop) → (∀ m (h : m < n + 1), p m h) ↔ p 0 (by omega) ∧ (∀ m (h : m < n), p (m + 1) (by omega))) +q((n : Nat) → (p : Nat → Prop) → (∀ m, m < n + 1 → p m) ↔ p 0 ∧ (∀ m, m < n → p (m + 1))) +q((n : Nat) → (p : (m : Nat) → (m < n + 1) → Prop) → (∃ m, ∃ (h : m < n + 1), p m h) ↔ (∃ m, ∃ (h : m < n), p m (by omega)) ∨ p n (by omega)) +q((n : Nat) → (p : Nat → Prop) → (∃ m, m < n + 1 ∧ p m) ↔ (∃ m, m < n ∧ p m) ∨ p n) +q((n : Nat) → (p : (m : Nat) → (m < n + 1) → Prop) → (∃ m, ∃ (h : m < n + 1), p m h) ↔ p 0 (by omega) ∨ (∃ m, ∃ (h : m < n), p (m + 1) (by omega))) +q((n : Nat) → (p : Nat → Prop) → (∃ m, m < n + 1 ∧ p m) ↔ p 0 ∨ (∃ m, m < n ∧ p (m + 1))) +q((a b c d : Nat) → (a + b) + (c + d) = (a + c) + (b + d)) +q((n : Nat) → 1 + n = n.succ) +q((n : Nat) → n.succ = 1 + n) +q((a b : Nat) → a.succ + b = a + b.succ) +q((n m : Nat) → n + m = 0 → n = 0) +q((n m : Nat) → n + m = 0 ↔ n = 0 ∧ m = 0) +q((n m k : Nat) → n + m = n + k ↔ m = k) +q((n m k : Nat) → m + n = k + n ↔ m = k) +q((a b : Nat) → a + b = b ↔ a = 0) +q((a b : Nat) → a + b = a ↔ b = 0) +q((a b : Nat) → a = a + b ↔ b = 0) +q((a b : Nat) → a = b + a ↔ b = 0) +q((n m k : Nat) → n + m ≤ n + k ↔ m ≤ k) +q((k n m : Nat) → k + n < m + n → k < m) +q((n k m : Nat) → n + k < n + m → k < m) +q((k n m : Nat) → k + n < k + m ↔ n < m) +q((k n m : Nat) → n + k < m + k ↔ n < m) +q((a b c d : Nat) → a ≤ b → c < d → a + c < b + d) +q((a b c d : Nat) → a < b → c ≤ d → a + c < b + d) +q((n k : Nat) → n < n + k → 0 < k) +q((n k : Nat) → n < k + n → 0 < k) +q((n k : Nat) → n < n + k ↔ 0 < k) +q((n k : Nat) → n < k + n ↔ 0 < k) +q((m n : Nat) → 0 < m → 0 < m + n) +q((m n : Nat) → 0 < n → 0 < m + n) +q((n : Nat) → n + n ≠ 1) +q((n : Nat) → n - 1 = n.pred) +q((n : Nat) → 1 - n = if n = 0 then 1 else 0) +q((n m k : Nat) → n.succ - m - k.succ = n - m - k) +q((n m k l : Nat) → (n + l) - m - (k + l) = n - m - k) +q((m n k : Nat) → m - n - k = m - k - n) +q((n m : Nat) → (n + m) - m = n) +q((n m : Nat) → m ≤ n → m + (n - m) = n) +q((n : Nat) → n.succ - 1 = n) +q((n : Nat) → (1 + n) - 1 = n) +q((n m : Nat) → m ≤ n → n - (n - m) = m) +q((n m k : Nat) → k ≤ n → n + m - k = n - k + m) +q((n m : Nat) → n - m = 0 ↔ n ≤ m) +q((n m : Nat) → 0 < n - m ↔ m < n) +q((a b c : Nat) → a - b ≤ c ↔ a ≤ c + b) +q((a b c : Nat) → a - b ≤ c ↔ a ≤ b + c) +q((n k m : Nat) → k ≤ m → n ≤ m - k ↔ n + k ≤ m) +q((n m : Int) → m + 1 ≠ 0 → n ≠ 0 → Int.lcm (m + 1) n ≠ 0) +q({a : Int} → a ∣ Int.lcm a 1) +q({a : Int} → 1 ∣ Int.lcm a 1 ) \ No newline at end of file diff --git a/data/test_set_B_tactic_step.sql.tar.gz b/data/test_set_B_tactic_step.sql.tar.gz new file mode 100644 index 0000000..27a0b6a --- /dev/null +++ b/data/test_set_B_tactic_step.sql.tar.gz @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:6dc1e729b1e023edd001c9eb4c10b7d6806a5a43f20d7186b860545a9f0ab9d8 +size 129995311 From 353bcc50e0ecf602761ff1ee9ed4a3134049e888 Mon Sep 17 00:00:00 2001 From: userName Date: Fri, 24 Apr 2026 13:19:55 +0800 Subject: [PATCH 2/2] Remove database owner from Test Set B dump --- data/test_set_B_tactic_step.sql.tar.gz | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/data/test_set_B_tactic_step.sql.tar.gz b/data/test_set_B_tactic_step.sql.tar.gz index 27a0b6a..ebb4564 100644 --- a/data/test_set_B_tactic_step.sql.tar.gz +++ b/data/test_set_B_tactic_step.sql.tar.gz @@ -1,3 +1,3 @@ version https://git-lfs.github.com/spec/v1 -oid sha256:6dc1e729b1e023edd001c9eb4c10b7d6806a5a43f20d7186b860545a9f0ab9d8 -size 129995311 +oid sha256:aa043a96dd494097407c0469bf39acbf84bae4e2499abad6640b58cf119987be +size 129584513