From 69c5b788b92c5876ea0bfe3ff3e5772564b98d7f Mon Sep 17 00:00:00 2001 From: Claude Bot Date: Fri, 18 Sep 2026 19:36:18 +0000 Subject: [PATCH] Generate the citable premise database, and goal-driven retrieval over it The database was the missing half: extraction and assembly existed, but nothing turned the book's main-content statements into something an agent could actually cite mid-proof, and nothing searched it. Two new scripts. textbook/build_database.py takes the main-content statements and emits both halves of a usable premise library: - an importable Lean file where every entry is a named declaration, so a proof can cite goodman_1_6_20 by name; - a JSONL search index carrying each entry's name, statement, mentioned identifiers and status. An entry is emitted as an `axiom` (asserted from the textbook) until a real lean-bench run proves it; passing --results upgrades those entries to real theorems carrying the exact verified proof. This mirrors how the book itself works -- its exercises are posed assuming its body results, the same way using Mathlib does not mean re-proving Mathlib. The cost is explicit: anything proven through an axiom inherits it, so a garbled extraction asserted as an axiom makes downstream proofs worthless. Guards: --require-checked refuses entries that have not passed check_statements.py (all 21 section 1.6 entries have, and are now marked accordingly), and the verifier's existing #print axioms check surfaces what a finished proof rests on. textbook/search_database.py is the retrieval step the proof loop calls at each line: given the current goal, it ranks premises by identifier and symbol overlap, weighting rare identifiers far above common ones (IsGCDOfList matching means much more than Int matching), preferring a proven premise over an asserted one, and formats the top few for the prompt. Verified against three real goals: the exactly-applicable premise tops each ranking by a wide margin (11.4 vs 1.6 for the gcd goal, 5.1 vs 3.7 for the prime-divides-product goal). It is a ranking heuristic, not a decision procedure -- only Lean can say whether a premise applies. Replacing score_premise() is the whole job of swapping in embeddings. Also: renamed library_candidates/ to database/ to match what it is; generated lib/Goodman/Chapter01Section06.lean (21 premises, 0 proven, 21 asserted) and database/goodman-1.6.index.jsonl; noted a latent bug in the older build_library.py, which attaches each entry's non-import prelude per-theorem and so would emit a shared `def` twice in one file -- build_database.py hoists and dedupes, and has a test pinning that. 13 new tests, all green (33 total, the one failure remains the pre-existing unrelated lean_agent import error in test_dataset.py). Still not done, and worth being clear about: nothing has been proven yet. The bench targets have not been elaboration-checked, no lean-bench run has happened over either file, and the goal-directed loop that would consume this retrieval does not exist -- lean-bench's solve() is still single-shot. Separately, lean-bench cannot currently run at all in this checkout, because lean_bench/cli.py imports lean_agent at module load and lean-agent is not installed. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_017vbLFFJiHSZqGZHEkjvG5x --- .gitignore | 1 + README.md | 4 +- database/goodman-1.6.index.jsonl | 21 +++ .../goodman-1.6.jsonl | 42 ++--- lib/Goodman/Chapter01Section06.lean | 73 ++++++++ tests/test_build_database.py | 69 ++++++++ tests/test_search_database.py | 58 +++++++ textbook/README.md | 77 +++++--- textbook/build_database.py | 164 ++++++++++++++++++ textbook/search_database.py | 99 +++++++++++ 10 files changed, 557 insertions(+), 51 deletions(-) create mode 100644 database/goodman-1.6.index.jsonl rename {library_candidates => database}/goodman-1.6.jsonl (90%) create mode 100644 lib/Goodman/Chapter01Section06.lean create mode 100644 tests/test_build_database.py create mode 100644 tests/test_search_database.py create mode 100644 textbook/build_database.py create mode 100644 textbook/search_database.py diff --git a/.gitignore b/.gitignore index ff9fae4..704cc77 100644 --- a/.gitignore +++ b/.gitignore @@ -10,3 +10,4 @@ results/ textbook/*.txt textbook/*_raw.txt .DS_Store +textbook/*.elab-report.jsonl diff --git a/README.md b/README.md index 02f4187..4b3caaa 100644 --- a/README.md +++ b/README.md @@ -31,14 +31,14 @@ mock 返回固定证明，仍由真实 Lean 检查。真实 LLM 需配置 endpoi `textbook/` 下有一套从教材 PDF 生成两类数据的工具：真正的 bench 目标（来自每节 的 Exercises，`datasets/`）和候选库（来自正文 Theorem/Proposition/Lemma/ -Corollary，`library_candidates/`，只有被真正证明过之后才进最终的可复用 Lean 库 +Corollary，`database/`，只有被真正证明过之后才进最终的可复用 Lean 库 文件），配 Definition 清单（Mathlib 没有的概念会编译成真正可导入的 Lean 代码， `lib/Definitions.lean`，不只是 JSON 元数据）。用法见 [textbook/README.md](textbook/README.md)。 ## 状态（更新于 2026-09-18） -`library_candidates/goodman-1.6.jsonl`（正文来源的候选库，21 条）全部通过本地 +`database/goodman-1.6.jsonl`（正文来源的候选库，21 条）全部通过本地 Lean elaboration 检查。`datasets/goodman-1.6-exercises.jsonl`（Exercises 1.6 来 源的真正 bench 目标，14 条）刚生成，尚待你本机跑一遍 `check_statements.py` 验 证。两边定义清单中的幻觉 Mathlib 引用均已修正。 diff --git a/database/goodman-1.6.index.jsonl b/database/goodman-1.6.index.jsonl new file mode 100644 index 0000000..6d08804 --- /dev/null +++ b/database/goodman-1.6.index.jsonl @@ -0,0 +1,21 @@ +{"name": "goodman_1_6_1", "id": "goodman-1-6-1", "source_label": "Proposition 1.6.1", "kind": "proposition", "status": "asserted", "statement": "∀ (a b c : ℤ), (a + b = b + a) ∧ (a + (b + c) = (a + b) + c) ∧ (0 + a = a) ∧ (a + (-a) = 0) ∧ (a * b = b * a) ∧ (a * (b * c) = (a * b) * c) ∧ (1 * a = a) ∧ (a * (b + c) = a * b + a * c) ∧ (∀ (x y : ℤ), x * y ≠ 0 → x ≠ 0 ∧ y ≠ 0)", "natural_language": "Addition and multiplication on the integers are commutative and associative, 0 and 1 are their respective identities, the distributive law holds, and a product of integers is nonzero iff both factors are nonzero.", "identifiers": [], "requires": ["Int.add_comm", "Int.add_assoc", "Int.zero_add", "Int.add_left_neg", "Int.mul_comm", "Int.mul_assoc", "Int.one_mul", "Int.mul_add", "Int.mul_ne_zero"]} +{"name": "goodman_1_6_4", "id": "goodman-1-6-4", "source_label": "Proposition 1.6.4", "kind": "proposition", "status": "asserted", "statement": "∀ (n : ℕ), n > 1 → ∃ (p : ℕ) (h : Nat.Prime p), p ∣ n", "natural_language": "Any natural number greater than 1 can be written as a product of prime numbers.", "identifiers": ["Nat.Prime"], "requires": ["Nat.exists_prime_factor"]} +{"name": "goodman_1_6_6", "id": "goodman-1-6-6", "source_label": "Theorem 1.6.6", "kind": "theorem", "status": "asserted", "statement": "∃ (p : ℕ → ℕ), ∀ (n : ℕ), Nat.Prime (p n) ∧ ∀ (i j : ℕ), i ≠ j → p i ≠ p j", "natural_language": "There are infinitely many prime numbers.", "identifiers": ["Nat.Prime"], "requires": ["Nat.infinite_primes"]} +{"name": "goodman_1_6_7", "id": "goodman-1-6-7", "source_label": "Proposition 1.6.7", "kind": "proposition", "status": "asserted", "statement": "∀ (a d : ℤ), d ≥ 1 → ∃! qr : ℤ × ℤ, a = qr.1 * d + qr.2 ∧ 0 ≤ qr.2 ∧ qr.2 < d", "natural_language": "Given integers a and d with d ≥ 1, there exist unique integers q and r such that a = qd + r and 0 ≤ r < d.", "identifiers": ["qr"], "requires": ["Int.division_theorem"]} +{"name": "goodman_1_6_9", "id": "goodman-1-6-9", "source_label": "Proposition 1.6.9", "kind": "proposition", "status": "asserted", "statement": "∀ (m n : ℤ), let I := {v : ℤ | ∃ a b : ℤ, v = a * m + b * n}; (∀ x ∈ I, ∀ y ∈ I, x + y ∈ I) ∧ (∀ x ∈ I, -x ∈ I) ∧ (∀ x : ℤ, ∀ z ∈ I, x * z ∈ I) ∧ (∀ b : ℤ, b ∣ m ∧ b ∣ n → ∀ z ∈ I, b ∣ z)", "natural_language": "I(m,n) = {am+bn} is closed under addition and negation, absorbs multiplication by any integer, and any common divisor of m and n divides every element of I(m,n).", "identifiers": [], "requires": []} +{"name": "goodman_1_6_10", "id": "goodman-1-6-10", "source_label": "Lemma 1.6.10", "kind": "lemma", "status": "asserted", "statement": "∀ (m n d : ℤ), d ∣ m ∧ d ∣ n ∧ d ∈ {v : ℤ | ∃ a b : ℤ, v = a * m + b * n} → ∀ (x : ℤ), x ∣ m ∧ x ∣ n → x ∣ d", "natural_language": "If a natural number d is a common divisor of m and n and an element of I(m, n), then d is the greatest common divisor of m and n.", "identifiers": [], "requires": ["Int.gcd_is_greatest_common_divisor"]} +{"name": "goodman_1_6_11", "id": "goodman-1-6-11", "source_label": "Proposition 1.6.11", "kind": "proposition", "status": "asserted", "statement": "∀ (m n : ℤ), m ≠ 0 ∧ n ≠ 0 → let d := Nat.gcd (Int.natAbs m) (Int.natAbs n); (d : ℤ) = Int.gcd m n ∧ (d : ℤ) ∈ {v : ℤ | ∃ a b : ℤ, v = a * m + b * n}", "natural_language": "The natural number d, which is the greatest common divisor of the absolute values of m and n, is also the greatest common divisor of m and n, and d is an element of I(m, n).", "identifiers": ["Nat.gcd", "Int.natAbs", "Int.gcd"], "requires": ["Int.gcd_nat_abs", "Int.gcd_linear_combination"]} +{"name": "goodman_1_6_13", "id": "goodman-1-6-13", "source_label": "Corollary 1.6.13", "kind": "corollary", "status": "asserted", "statement": "∀ (m n : ℤ), m ≠ 0 → n ≠ 0 → let I := {v : ℤ | ∃ a b : ℤ, v = a * m + b * n}; let d := Int.gcd m n; IsLeast {x : ℤ | 0 < x ∧ x ∈ I} (d : ℤ) ∧ I = {v : ℤ | ∃ k : ℤ, v = k * d}", "natural_language": "gcd(m,n) is the least positive element of I(m,n), and I(m,n) is exactly the set of integer multiples of gcd(m,n).", "identifiers": ["Int.gcd", "IsLeast"], "requires": ["IsLeast", "Int.gcd"]} +{"name": "goodman_1_6_15", "id": "goodman-1-6-15", "source_label": "Corollary 1.6.15", "kind": "corollary", "status": "asserted", "statement": "∀ (m n : ℤ), m ≠ 0 ∧ n ≠ 0 → Int.gcd m n = 1 ↔ ∃ (s t : ℤ), s * m + t * n = 1", "natural_language": "Two nonzero integers m and n are relatively prime if and only if there exist integers s and t such that sm + tn = 1.", "identifiers": ["Int.gcd"], "requires": ["Int.coprime_iff_gcd_eq_one"]} +{"name": "goodman_1_6_17", "id": "goodman-1-6-17", "source_label": "Corollary 1.6.17", "kind": "corollary", "status": "asserted", "statement": "∀ (a b : ℕ) (x : ℤ), Nat.Coprime a b ∧ (a:ℤ) ∣ x ∧ (b:ℤ) ∣ x → (a:ℤ) * b ∣ x", "natural_language": "If a and b are relatively prime natural numbers and both divide an integer x, then their product ab also divides x.", "identifiers": ["Nat.Coprime"], "requires": ["Nat.coprime_mul_dvd"]} +{"name": "goodman_1_6_18", "id": "goodman-1-6-18", "source_label": "Proposition 1.6.18", "kind": "proposition", "status": "asserted", "statement": "∀ (p : ℕ) (a : ℤ), Nat.Prime p ∧ a ≠ 0 → (p:ℤ) ∣ a ∨ IsCoprime (p:ℤ) a", "natural_language": "If p is a prime number and a is any nonzero integer, then either p divides a or p and a are relatively prime.", "identifiers": ["Nat.Prime", "IsCoprime"], "requires": ["Int.prime_or_coprime"]} +{"name": "goodman_1_6_19", "id": "goodman-1-6-19", "source_label": "Proposition 1.6.19", "kind": "proposition", "status": "asserted", "statement": "∀ (p : ℕ) (a b : ℤ), Nat.Prime p ∧ a ≠ 0 ∧ b ≠ 0 → (p:ℤ) ∣ a * b → (p:ℤ) ∣ a ∨ (p:ℤ) ∣ b", "natural_language": "If p is a prime number and a and b are nonzero integers, and p divides the product ab, then p divides a or p divides b.", "identifiers": ["Nat.Prime"], "requires": ["Int.prime_dvd_mul"]} +{"name": "goodman_1_6_20", "id": "goodman-1-6-20", "source_label": "Corollary 1.6.20", "kind": "corollary", "status": "asserted", "statement": "∀ (p : ℕ) (as : List ℤ), Nat.Prime p → (∀ (a : ℤ), a ∈ as → a ≠ 0) → (p:ℤ) ∣ List.prod as → ∃ (a : ℤ), a ∈ as ∧ (p:ℤ) ∣ a", "natural_language": "If a prime number p divides a product of nonzero integers, then p divides one of the factors.", "identifiers": ["as", "List", "Nat.Prime", "List.prod"], "requires": ["Int.prime_dvd_prod"]} +{"name": "goodman_1_6_21", "id": "goodman-1-6-21", "source_label": "Theorem 1.6.21", "kind": "theorem", "status": "asserted", "statement": "∀ (n : ℕ), n > 1 → ∃! (ps : List ℕ), (∀ (p : ℕ), p ∈ ps → Nat.Prime p) ∧ n = List.prod ps", "natural_language": "The prime factorization of a natural number is unique.", "identifiers": ["ps", "List", "Nat.Prime", "List.prod"], "requires": ["Nat.unique_prime_factorization"]} +{"name": "goodman_1_6_23", "id": "goodman-1-6-23", "source_label": "Lemma 1.6.23", "kind": "lemma", "status": "asserted", "statement": "∀ (n : ℕ) (a : Fin n → ℤ), 2 ≤ n → (∀ i, a i ≠ 0) → ∃ (d : ℕ) (Q : Matrix (Fin n) (Fin n) ℤ), IsUnit Q.det ∧ ∀ j : Fin n, Matrix.vecMul a Q j = if j.val = 0 then (d : ℤ) else 0", "natural_language": "Given n >= 2 nonzero integers a_1..a_n, there is a natural number d and a unimodular (det a unit, i.e. det = +-1) integer n-by-n matrix Q such that the row vector a times Q equals (d, 0, ..., 0).", "identifiers": ["Fin", "Matrix", "IsUnit", "Q.det", "Matrix.vecMul", "j.val"], "requires": ["Matrix.vecMul", "Matrix.det", "IsUnit"]} +{"name": "goodman_1_6_24", "id": "goodman-1-6-24", "source_label": "Proposition 1.6.24", "kind": "proposition", "status": "asserted", "statement": "∀ (as : List ℤ), as.length ≥ 2 → (∀ (a : ℤ), a ∈ as → a ≠ 0) → ∃ (d : ℕ) (cs : List ℤ), IsGCDOfList d as ∧ (d:ℤ) = List.sum (List.zipWith (· * ·) cs as)", "natural_language": "The greatest common divisor of a list of at least two nonzero integers exists and is an integer linear combination of the integers in the list.", "identifiers": ["as", "List", "as.length", "cs", "IsGCDOfList", "List.sum", "List.zipWith"], "requires": ["GCD.gcd_exists", "GCD.gcd_linear_combination"]} +{"name": "goodman_1_6_26", "id": "goodman-1-6-26", "source_label": "Lemma 1.6.26", "kind": "lemma", "status": "asserted", "statement": "∀ (as : List ℤ) (z : ℤ), as.length ≥ 2 → (∀ (i j : ℕ), i ≠ j → i < as.length → j < as.length → IsCoprime (as[i]) (as[j])) → (∀ (a : ℤ), a ∈ as → a ≠ 0) → (∀ (a : ℤ), a ∈ as → a ∣ z) → List.prod as ∣ z", "natural_language": "If a list of integers is pairwise relatively prime and each integer in the list divides an integer z, then the product of the integers in the list also divides z.", "identifiers": ["as", "List", "as.length", "IsCoprime", "List.prod"], "requires": ["Int.pairwise_coprime_mul_dvd"]} +{"name": "goodman_1_6_2_a", "id": "goodman-1-6-2-a", "source_label": "Proposition 1.6.2", "kind": "proposition", "status": "asserted", "statement": "∀ (u v : ℤ), u * v = 1 → (u = 1 ∧ v = 1) ∨ (u = -1 ∧ v = -1)", "natural_language": "If two integers multiply to 1, both are 1 or both are -1.", "identifiers": [], "requires": ["Int.eq_one_or_self_of_prime"]} +{"name": "goodman_1_6_2_b", "id": "goodman-1-6-2-b", "source_label": "Proposition 1.6.2", "kind": "proposition", "status": "asserted", "statement": "∀ (a b : ℤ), a ∣ b ∧ b ∣ a → a = b ∨ a = -b", "natural_language": "If two integers divide each other, they are equal or negatives of each other.", "identifiers": [], "requires": ["Int.dvd_antisymm"]} +{"name": "goodman_1_6_2_c", "id": "goodman-1-6-2-c", "source_label": "Proposition 1.6.2", "kind": "proposition", "status": "asserted", "statement": "∀ (a b c : ℤ), a ∣ b ∧ b ∣ c → a ∣ c", "natural_language": "Divisibility of integers is transitive.", "identifiers": [], "requires": ["Int.dvd_trans"]} +{"name": "goodman_1_6_2_d", "id": "goodman-1-6-2-d", "source_label": "Proposition 1.6.2", "kind": "proposition", "status": "asserted", "statement": "∀ (a b c s t : ℤ), a ∣ b ∧ a ∣ c → a ∣ (s * b + t * c)", "natural_language": "If an integer divides two others, it divides any integer linear combination of them.", "identifiers": [], "requires": ["dvd_add", "Dvd.dvd.mul_left"]} diff --git a/library_candidates/goodman-1.6.jsonl b/database/goodman-1.6.jsonl similarity index 90% rename from library_candidates/goodman-1.6.jsonl rename to database/goodman-1.6.jsonl index 055c7aa..318777c 100644 --- a/library_candidates/goodman-1.6.jsonl +++ b/database/goodman-1.6.jsonl @@ -1,21 +1,21 @@ -{"id": "goodman-1-6-1", "source_label": "Proposition 1.6.1", "kind": "proposition", "statement": "∀ (a b c : ℤ), (a + b = b + a) ∧ (a + (b + c) = (a + b) + c) ∧ (0 + a = a) ∧ (a + (-a) = 0) ∧ (a * b = b * a) ∧ (a * (b * c) = (a * b) * c) ∧ (1 * a = a) ∧ (a * (b + c) = a * b + a * c) ∧ (∀ (x y : ℤ), x * y ≠ 0 → x ≠ 0 ∧ y ≠ 0)", "prelude": "import Mathlib", "natural_language": "Addition and multiplication on the integers are commutative and associative, 0 and 1 are their respective identities, the distributive law holds, and a product of integers is nonzero iff both factors are nonzero.", "requires": ["Int.add_comm", "Int.add_assoc", "Int.zero_add", "Int.add_left_neg", "Int.mul_comm", "Int.mul_assoc", "Int.one_mul", "Int.mul_add", "Int.mul_ne_zero"], "include_in_bench": true, "exclude_reason": null} -{"id": "goodman-1-6-4", "source_label": "Proposition 1.6.4", "kind": "proposition", "statement": "∀ (n : ℕ), n > 1 → ∃ (p : ℕ) (h : Nat.Prime p), p ∣ n", "prelude": "import Mathlib", "natural_language": "Any natural number greater than 1 can be written as a product of prime numbers.", "requires": ["Nat.exists_prime_factor"], "include_in_bench": true, "exclude_reason": null} -{"id": "goodman-1-6-6", "source_label": "Theorem 1.6.6", "kind": "theorem", "statement": "∃ (p : ℕ → ℕ), ∀ (n : ℕ), Nat.Prime (p n) ∧ ∀ (i j : ℕ), i ≠ j → p i ≠ p j", "prelude": "import Mathlib", "natural_language": "There are infinitely many prime numbers.", "requires": ["Nat.infinite_primes"], "include_in_bench": true, "exclude_reason": null} -{"id": "goodman-1-6-7", "source_label": "Proposition 1.6.7", "kind": "proposition", "statement": "∀ (a d : ℤ), d ≥ 1 → ∃! qr : ℤ × ℤ, a = qr.1 * d + qr.2 ∧ 0 ≤ qr.2 ∧ qr.2 < d", "prelude": "import Mathlib", "natural_language": "Given integers a and d with d ≥ 1, there exist unique integers q and r such that a = qd + r and 0 ≤ r < d.", "requires": ["Int.division_theorem"], "include_in_bench": true, "exclude_reason": null} -{"id": "goodman-1-6-9", "source_label": "Proposition 1.6.9", "kind": "proposition", "statement": "∀ (m n : ℤ), let I := {v : ℤ | ∃ a b : ℤ, v = a * m + b * n}; (∀ x ∈ I, ∀ y ∈ I, x + y ∈ I) ∧ (∀ x ∈ I, -x ∈ I) ∧ (∀ x : ℤ, ∀ z ∈ I, x * z ∈ I) ∧ (∀ b : ℤ, b ∣ m ∧ b ∣ n → ∀ z ∈ I, b ∣ z)", "prelude": "import Mathlib", "natural_language": "I(m,n) = {am+bn} is closed under addition and negation, absorbs multiplication by any integer, and any common divisor of m and n divides every element of I(m,n).", "requires": [], "include_in_bench": true, "exclude_reason": null} -{"id": "goodman-1-6-10", "source_label": "Lemma 1.6.10", "kind": "lemma", "statement": "∀ (m n d : ℤ), d ∣ m ∧ d ∣ n ∧ d ∈ {v : ℤ | ∃ a b : ℤ, v = a * m + b * n} → ∀ (x : ℤ), x ∣ m ∧ x ∣ n → x ∣ d", "prelude": "import Mathlib", "natural_language": "If a natural number d is a common divisor of m and n and an element of I(m, n), then d is the greatest common divisor of m and n.", "requires": ["Int.gcd_is_greatest_common_divisor"], "include_in_bench": true, "exclude_reason": null} -{"id": "goodman-1-6-11", "source_label": "Proposition 1.6.11", "kind": "proposition", "statement": "∀ (m n : ℤ), m ≠ 0 ∧ n ≠ 0 → let d := Nat.gcd (Int.natAbs m) (Int.natAbs n); (d : ℤ) = Int.gcd m n ∧ (d : ℤ) ∈ {v : ℤ | ∃ a b : ℤ, v = a * m + b * n}", "prelude": "import Mathlib", "natural_language": "The natural number d, which is the greatest common divisor of the absolute values of m and n, is also the greatest common divisor of m and n, and d is an element of I(m, n).", "requires": ["Int.gcd_nat_abs", "Int.gcd_linear_combination"], "include_in_bench": true, "exclude_reason": null} -{"id": "goodman-1-6-13", "source_label": "Corollary 1.6.13", "kind": "corollary", "statement": "∀ (m n : ℤ), m ≠ 0 → n ≠ 0 → let I := {v : ℤ | ∃ a b : ℤ, v = a * m + b * n}; let d := Int.gcd m n; IsLeast {x : ℤ | 0 < x ∧ x ∈ I} (d : ℤ) ∧ I = {v : ℤ | ∃ k : ℤ, v = k * d}", "prelude": "import Mathlib", "natural_language": "gcd(m,n) is the least positive element of I(m,n), and I(m,n) is exactly the set of integer multiples of gcd(m,n).", "requires": ["IsLeast", "Int.gcd"], "include_in_bench": true, "exclude_reason": null} -{"id": "goodman-1-6-15", "source_label": "Corollary 1.6.15", "kind": "corollary", "statement": "∀ (m n : ℤ), m ≠ 0 ∧ n ≠ 0 → Int.gcd m n = 1 ↔ ∃ (s t : ℤ), s * m + t * n = 1", "prelude": "import Mathlib", "natural_language": "Two nonzero integers m and n are relatively prime if and only if there exist integers s and t such that sm + tn = 1.", "requires": ["Int.coprime_iff_gcd_eq_one"], "include_in_bench": true, "exclude_reason": null} -{"id": "goodman-1-6-17", "source_label": "Corollary 1.6.17", "kind": "corollary", "statement": "∀ (a b : ℕ) (x : ℤ), Nat.Coprime a b ∧ (a:ℤ) ∣ x ∧ (b:ℤ) ∣ x → (a:ℤ) * b ∣ x", "prelude": "import Mathlib", "natural_language": "If a and b are relatively prime natural numbers and both divide an integer x, then their product ab also divides x.", "requires": ["Nat.coprime_mul_dvd"], "include_in_bench": true, "exclude_reason": null} -{"id": "goodman-1-6-18", "source_label": "Proposition 1.6.18", "kind": "proposition", "statement": "∀ (p : ℕ) (a : ℤ), Nat.Prime p ∧ a ≠ 0 → (p:ℤ) ∣ a ∨ IsCoprime (p:ℤ) a", "prelude": "import Mathlib", "natural_language": "If p is a prime number and a is any nonzero integer, then either p divides a or p and a are relatively prime.", "requires": ["Int.prime_or_coprime"], "include_in_bench": true, "exclude_reason": null} -{"id": "goodman-1-6-19", "source_label": "Proposition 1.6.19", "kind": "proposition", "statement": "∀ (p : ℕ) (a b : ℤ), Nat.Prime p ∧ a ≠ 0 ∧ b ≠ 0 → (p:ℤ) ∣ a * b → (p:ℤ) ∣ a ∨ (p:ℤ) ∣ b", "prelude": "import Mathlib", "natural_language": "If p is a prime number and a and b are nonzero integers, and p divides the product ab, then p divides a or p divides b.", "requires": ["Int.prime_dvd_mul"], "include_in_bench": true, "exclude_reason": null} -{"id": "goodman-1-6-20", "source_label": "Corollary 1.6.20", "kind": "corollary", "statement": "∀ (p : ℕ) (as : List ℤ), Nat.Prime p → (∀ (a : ℤ), a ∈ as → a ≠ 0) → (p:ℤ) ∣ List.prod as → ∃ (a : ℤ), a ∈ as ∧ (p:ℤ) ∣ a", "prelude": "import Mathlib", "natural_language": "If a prime number p divides a product of nonzero integers, then p divides one of the factors.", "requires": ["Int.prime_dvd_prod"], "include_in_bench": true, "exclude_reason": null} -{"id": "goodman-1-6-21", "source_label": "Theorem 1.6.21", "kind": "theorem", "statement": "∀ (n : ℕ), n > 1 → ∃! (ps : List ℕ), (∀ (p : ℕ), p ∈ ps → Nat.Prime p) ∧ n = List.prod ps", "prelude": "import Mathlib", "natural_language": "The prime factorization of a natural number is unique.", "requires": ["Nat.unique_prime_factorization"], "include_in_bench": true, "exclude_reason": null} -{"id": "goodman-1-6-23", "source_label": "Lemma 1.6.23", "kind": "lemma", "statement": "∀ (n : ℕ) (a : Fin n → ℤ), 2 ≤ n → (∀ i, a i ≠ 0) → ∃ (d : ℕ) (Q : Matrix (Fin n) (Fin n) ℤ), IsUnit Q.det ∧ ∀ j : Fin n, Matrix.vecMul a Q j = if j.val = 0 then (d : ℤ) else 0", "prelude": "import Mathlib", "natural_language": "Given n >= 2 nonzero integers a_1..a_n, there is a natural number d and a unimodular (det a unit, i.e. det = +-1) integer n-by-n matrix Q such that the row vector a times Q equals (d, 0, ..., 0).", "requires": ["Matrix.vecMul", "Matrix.det", "IsUnit"], "include_in_bench": true, "exclude_reason": null} -{"id": "goodman-1-6-24", "source_label": "Proposition 1.6.24", "kind": "proposition", "statement": "∀ (as : List ℤ), as.length ≥ 2 → (∀ (a : ℤ), a ∈ as → a ≠ 0) → ∃ (d : ℕ) (cs : List ℤ), IsGCDOfList d as ∧ (d:ℤ) = List.sum (List.zipWith (· * ·) cs as)", "prelude": "import Mathlib\ndef IsGCDOfList (d : ℕ) (as : List ℤ) : Prop :=\n (∀ a ∈ as, (d:ℤ) ∣ a) ∧ ∀ e : ℤ, (∀ a ∈ as, e ∣ a) → e ∣ (d:ℤ)", "natural_language": "The greatest common divisor of a list of at least two nonzero integers exists and is an integer linear combination of the integers in the list.", "requires": ["GCD.gcd_exists", "GCD.gcd_linear_combination"], "include_in_bench": true, "exclude_reason": null} -{"id": "goodman-1-6-26", "source_label": "Lemma 1.6.26", "kind": "lemma", "statement": "∀ (as : List ℤ) (z : ℤ), as.length ≥ 2 → (∀ (i j : ℕ), i ≠ j → i < as.length → j < as.length → IsCoprime (as[i]) (as[j])) → (∀ (a : ℤ), a ∈ as → a ≠ 0) → (∀ (a : ℤ), a ∈ as → a ∣ z) → List.prod as ∣ z", "prelude": "import Mathlib", "natural_language": "If a list of integers is pairwise relatively prime and each integer in the list divides an integer z, then the product of the integers in the list also divides z.", "requires": ["Int.pairwise_coprime_mul_dvd"], "include_in_bench": true, "exclude_reason": null} -{"id": "goodman-1-6-2-a", "source_label": "Proposition 1.6.2", "kind": "proposition", "statement": "∀ (u v : ℤ), u * v = 1 → (u = 1 ∧ v = 1) ∨ (u = -1 ∧ v = -1)", "prelude": "import Mathlib", "natural_language": "If two integers multiply to 1, both are 1 or both are -1.", "requires": ["Int.eq_one_or_self_of_prime"], "include_in_bench": true, "exclude_reason": null} -{"id": "goodman-1-6-2-b", "source_label": "Proposition 1.6.2", "kind": "proposition", "statement": "∀ (a b : ℤ), a ∣ b ∧ b ∣ a → a = b ∨ a = -b", "prelude": "import Mathlib", "natural_language": "If two integers divide each other, they are equal or negatives of each other.", "requires": ["Int.dvd_antisymm"], "include_in_bench": true, "exclude_reason": null} -{"id": "goodman-1-6-2-c", "source_label": "Proposition 1.6.2", "kind": "proposition", "statement": "∀ (a b c : ℤ), a ∣ b ∧ b ∣ c → a ∣ c", "prelude": "import Mathlib", "natural_language": "Divisibility of integers is transitive.", "requires": ["Int.dvd_trans"], "include_in_bench": true, "exclude_reason": null} -{"id": "goodman-1-6-2-d", "source_label": "Proposition 1.6.2", "kind": "proposition", "statement": "∀ (a b c s t : ℤ), a ∣ b ∧ a ∣ c → a ∣ (s * b + t * c)", "prelude": "import Mathlib", "natural_language": "If an integer divides two others, it divides any integer linear combination of them.", "requires": ["dvd_add", "Dvd.dvd.mul_left"], "include_in_bench": true, "exclude_reason": null} +{"id": "goodman-1-6-1", "source_label": "Proposition 1.6.1", "kind": "proposition", "statement": "∀ (a b c : ℤ), (a + b = b + a) ∧ (a + (b + c) = (a + b) + c) ∧ (0 + a = a) ∧ (a + (-a) = 0) ∧ (a * b = b * a) ∧ (a * (b * c) = (a * b) * c) ∧ (1 * a = a) ∧ (a * (b + c) = a * b + a * c) ∧ (∀ (x y : ℤ), x * y ≠ 0 → x ≠ 0 ∧ y ≠ 0)", "prelude": "import Mathlib", "natural_language": "Addition and multiplication on the integers are commutative and associative, 0 and 1 are their respective identities, the distributive law holds, and a product of integers is nonzero iff both factors are nonzero.", "requires": ["Int.add_comm", "Int.add_assoc", "Int.zero_add", "Int.add_left_neg", "Int.mul_comm", "Int.mul_assoc", "Int.one_mul", "Int.mul_add", "Int.mul_ne_zero"], "include_in_bench": true, "exclude_reason": null, "elaborates": true} +{"id": "goodman-1-6-4", "source_label": "Proposition 1.6.4", "kind": "proposition", "statement": "∀ (n : ℕ), n > 1 → ∃ (p : ℕ) (h : Nat.Prime p), p ∣ n", "prelude": "import Mathlib", "natural_language": "Any natural number greater than 1 can be written as a product of prime numbers.", "requires": ["Nat.exists_prime_factor"], "include_in_bench": true, "exclude_reason": null, "elaborates": true} +{"id": "goodman-1-6-6", "source_label": "Theorem 1.6.6", "kind": "theorem", "statement": "∃ (p : ℕ → ℕ), ∀ (n : ℕ), Nat.Prime (p n) ∧ ∀ (i j : ℕ), i ≠ j → p i ≠ p j", "prelude": "import Mathlib", "natural_language": "There are infinitely many prime numbers.", "requires": ["Nat.infinite_primes"], "include_in_bench": true, "exclude_reason": null, "elaborates": true} +{"id": "goodman-1-6-7", "source_label": "Proposition 1.6.7", "kind": "proposition", "statement": "∀ (a d : ℤ), d ≥ 1 → ∃! qr : ℤ × ℤ, a = qr.1 * d + qr.2 ∧ 0 ≤ qr.2 ∧ qr.2 < d", "prelude": "import Mathlib", "natural_language": "Given integers a and d with d ≥ 1, there exist unique integers q and r such that a = qd + r and 0 ≤ r < d.", "requires": ["Int.division_theorem"], "include_in_bench": true, "exclude_reason": null, "elaborates": true} +{"id": "goodman-1-6-9", "source_label": "Proposition 1.6.9", "kind": "proposition", "statement": "∀ (m n : ℤ), let I := {v : ℤ | ∃ a b : ℤ, v = a * m + b * n}; (∀ x ∈ I, ∀ y ∈ I, x + y ∈ I) ∧ (∀ x ∈ I, -x ∈ I) ∧ (∀ x : ℤ, ∀ z ∈ I, x * z ∈ I) ∧ (∀ b : ℤ, b ∣ m ∧ b ∣ n → ∀ z ∈ I, b ∣ z)", "prelude": "import Mathlib", "natural_language": "I(m,n) = {am+bn} is closed under addition and negation, absorbs multiplication by any integer, and any common divisor of m and n divides every element of I(m,n).", "requires": [], "include_in_bench": true, "exclude_reason": null, "elaborates": true} +{"id": "goodman-1-6-10", "source_label": "Lemma 1.6.10", "kind": "lemma", "statement": "∀ (m n d : ℤ), d ∣ m ∧ d ∣ n ∧ d ∈ {v : ℤ | ∃ a b : ℤ, v = a * m + b * n} → ∀ (x : ℤ), x ∣ m ∧ x ∣ n → x ∣ d", "prelude": "import Mathlib", "natural_language": "If a natural number d is a common divisor of m and n and an element of I(m, n), then d is the greatest common divisor of m and n.", "requires": ["Int.gcd_is_greatest_common_divisor"], "include_in_bench": true, "exclude_reason": null, "elaborates": true} +{"id": "goodman-1-6-11", "source_label": "Proposition 1.6.11", "kind": "proposition", "statement": "∀ (m n : ℤ), m ≠ 0 ∧ n ≠ 0 → let d := Nat.gcd (Int.natAbs m) (Int.natAbs n); (d : ℤ) = Int.gcd m n ∧ (d : ℤ) ∈ {v : ℤ | ∃ a b : ℤ, v = a * m + b * n}", "prelude": "import Mathlib", "natural_language": "The natural number d, which is the greatest common divisor of the absolute values of m and n, is also the greatest common divisor of m and n, and d is an element of I(m, n).", "requires": ["Int.gcd_nat_abs", "Int.gcd_linear_combination"], "include_in_bench": true, "exclude_reason": null, "elaborates": true} +{"id": "goodman-1-6-13", "source_label": "Corollary 1.6.13", "kind": "corollary", "statement": "∀ (m n : ℤ), m ≠ 0 → n ≠ 0 → let I := {v : ℤ | ∃ a b : ℤ, v = a * m + b * n}; let d := Int.gcd m n; IsLeast {x : ℤ | 0 < x ∧ x ∈ I} (d : ℤ) ∧ I = {v : ℤ | ∃ k : ℤ, v = k * d}", "prelude": "import Mathlib", "natural_language": "gcd(m,n) is the least positive element of I(m,n), and I(m,n) is exactly the set of integer multiples of gcd(m,n).", "requires": ["IsLeast", "Int.gcd"], "include_in_bench": true, "exclude_reason": null, "elaborates": true} +{"id": "goodman-1-6-15", "source_label": "Corollary 1.6.15", "kind": "corollary", "statement": "∀ (m n : ℤ), m ≠ 0 ∧ n ≠ 0 → Int.gcd m n = 1 ↔ ∃ (s t : ℤ), s * m + t * n = 1", "prelude": "import Mathlib", "natural_language": "Two nonzero integers m and n are relatively prime if and only if there exist integers s and t such that sm + tn = 1.", "requires": ["Int.coprime_iff_gcd_eq_one"], "include_in_bench": true, "exclude_reason": null, "elaborates": true} +{"id": "goodman-1-6-17", "source_label": "Corollary 1.6.17", "kind": "corollary", "statement": "∀ (a b : ℕ) (x : ℤ), Nat.Coprime a b ∧ (a:ℤ) ∣ x ∧ (b:ℤ) ∣ x → (a:ℤ) * b ∣ x", "prelude": "import Mathlib", "natural_language": "If a and b are relatively prime natural numbers and both divide an integer x, then their product ab also divides x.", "requires": ["Nat.coprime_mul_dvd"], "include_in_bench": true, "exclude_reason": null, "elaborates": true} +{"id": "goodman-1-6-18", "source_label": "Proposition 1.6.18", "kind": "proposition", "statement": "∀ (p : ℕ) (a : ℤ), Nat.Prime p ∧ a ≠ 0 → (p:ℤ) ∣ a ∨ IsCoprime (p:ℤ) a", "prelude": "import Mathlib", "natural_language": "If p is a prime number and a is any nonzero integer, then either p divides a or p and a are relatively prime.", "requires": ["Int.prime_or_coprime"], "include_in_bench": true, "exclude_reason": null, "elaborates": true} +{"id": "goodman-1-6-19", "source_label": "Proposition 1.6.19", "kind": "proposition", "statement": "∀ (p : ℕ) (a b : ℤ), Nat.Prime p ∧ a ≠ 0 ∧ b ≠ 0 → (p:ℤ) ∣ a * b → (p:ℤ) ∣ a ∨ (p:ℤ) ∣ b", "prelude": "import Mathlib", "natural_language": "If p is a prime number and a and b are nonzero integers, and p divides the product ab, then p divides a or p divides b.", "requires": ["Int.prime_dvd_mul"], "include_in_bench": true, "exclude_reason": null, "elaborates": true} +{"id": "goodman-1-6-20", "source_label": "Corollary 1.6.20", "kind": "corollary", "statement": "∀ (p : ℕ) (as : List ℤ), Nat.Prime p → (∀ (a : ℤ), a ∈ as → a ≠ 0) → (p:ℤ) ∣ List.prod as → ∃ (a : ℤ), a ∈ as ∧ (p:ℤ) ∣ a", "prelude": "import Mathlib", "natural_language": "If a prime number p divides a product of nonzero integers, then p divides one of the factors.", "requires": ["Int.prime_dvd_prod"], "include_in_bench": true, "exclude_reason": null, "elaborates": true} +{"id": "goodman-1-6-21", "source_label": "Theorem 1.6.21", "kind": "theorem", "statement": "∀ (n : ℕ), n > 1 → ∃! (ps : List ℕ), (∀ (p : ℕ), p ∈ ps → Nat.Prime p) ∧ n = List.prod ps", "prelude": "import Mathlib", "natural_language": "The prime factorization of a natural number is unique.", "requires": ["Nat.unique_prime_factorization"], "include_in_bench": true, "exclude_reason": null, "elaborates": true} +{"id": "goodman-1-6-23", "source_label": "Lemma 1.6.23", "kind": "lemma", "statement": "∀ (n : ℕ) (a : Fin n → ℤ), 2 ≤ n → (∀ i, a i ≠ 0) → ∃ (d : ℕ) (Q : Matrix (Fin n) (Fin n) ℤ), IsUnit Q.det ∧ ∀ j : Fin n, Matrix.vecMul a Q j = if j.val = 0 then (d : ℤ) else 0", "prelude": "import Mathlib", "natural_language": "Given n >= 2 nonzero integers a_1..a_n, there is a natural number d and a unimodular (det a unit, i.e. det = +-1) integer n-by-n matrix Q such that the row vector a times Q equals (d, 0, ..., 0).", "requires": ["Matrix.vecMul", "Matrix.det", "IsUnit"], "include_in_bench": true, "exclude_reason": null, "elaborates": true} +{"id": "goodman-1-6-24", "source_label": "Proposition 1.6.24", "kind": "proposition", "statement": "∀ (as : List ℤ), as.length ≥ 2 → (∀ (a : ℤ), a ∈ as → a ≠ 0) → ∃ (d : ℕ) (cs : List ℤ), IsGCDOfList d as ∧ (d:ℤ) = List.sum (List.zipWith (· * ·) cs as)", "prelude": "import Mathlib\ndef IsGCDOfList (d : ℕ) (as : List ℤ) : Prop :=\n (∀ a ∈ as, (d:ℤ) ∣ a) ∧ ∀ e : ℤ, (∀ a ∈ as, e ∣ a) → e ∣ (d:ℤ)", "natural_language": "The greatest common divisor of a list of at least two nonzero integers exists and is an integer linear combination of the integers in the list.", "requires": ["GCD.gcd_exists", "GCD.gcd_linear_combination"], "include_in_bench": true, "exclude_reason": null, "elaborates": true} +{"id": "goodman-1-6-26", "source_label": "Lemma 1.6.26", "kind": "lemma", "statement": "∀ (as : List ℤ) (z : ℤ), as.length ≥ 2 → (∀ (i j : ℕ), i ≠ j → i < as.length → j < as.length → IsCoprime (as[i]) (as[j])) → (∀ (a : ℤ), a ∈ as → a ≠ 0) → (∀ (a : ℤ), a ∈ as → a ∣ z) → List.prod as ∣ z", "prelude": "import Mathlib", "natural_language": "If a list of integers is pairwise relatively prime and each integer in the list divides an integer z, then the product of the integers in the list also divides z.", "requires": ["Int.pairwise_coprime_mul_dvd"], "include_in_bench": true, "exclude_reason": null, "elaborates": true} +{"id": "goodman-1-6-2-a", "source_label": "Proposition 1.6.2", "kind": "proposition", "statement": "∀ (u v : ℤ), u * v = 1 → (u = 1 ∧ v = 1) ∨ (u = -1 ∧ v = -1)", "prelude": "import Mathlib", "natural_language": "If two integers multiply to 1, both are 1 or both are -1.", "requires": ["Int.eq_one_or_self_of_prime"], "include_in_bench": true, "exclude_reason": null, "elaborates": true} +{"id": "goodman-1-6-2-b", "source_label": "Proposition 1.6.2", "kind": "proposition", "statement": "∀ (a b : ℤ), a ∣ b ∧ b ∣ a → a = b ∨ a = -b", "prelude": "import Mathlib", "natural_language": "If two integers divide each other, they are equal or negatives of each other.", "requires": ["Int.dvd_antisymm"], "include_in_bench": true, "exclude_reason": null, "elaborates": true} +{"id": "goodman-1-6-2-c", "source_label": "Proposition 1.6.2", "kind": "proposition", "statement": "∀ (a b c : ℤ), a ∣ b ∧ b ∣ c → a ∣ c", "prelude": "import Mathlib", "natural_language": "Divisibility of integers is transitive.", "requires": ["Int.dvd_trans"], "include_in_bench": true, "exclude_reason": null, "elaborates": true} +{"id": "goodman-1-6-2-d", "source_label": "Proposition 1.6.2", "kind": "proposition", "statement": "∀ (a b c s t : ℤ), a ∣ b ∧ a ∣ c → a ∣ (s * b + t * c)", "prelude": "import Mathlib", "natural_language": "If an integer divides two others, it divides any integer linear combination of them.", "requires": ["dvd_add", "Dvd.dvd.mul_left"], "include_in_bench": true, "exclude_reason": null, "elaborates": true} diff --git a/lib/Goodman/Chapter01Section06.lean b/lib/Goodman/Chapter01Section06.lean new file mode 100644 index 0000000..1ccc07d --- /dev/null +++ b/lib/Goodman/Chapter01Section06.lean @@ -0,0 +1,73 @@ +-- Generated by textbook/build_database.py -- do not hand-edit. +-- Citable premise database from the textbook's main content. +-- `axiom` entries are asserted from the book, NOT proven here: anything +-- proven through one inherits it, so check `#print axioms` downstream. + +import Mathlib + +def IsGCDOfList (d : ℕ) (as : List ℤ) : Prop := + (∀ a ∈ as, (d:ℤ) ∣ a) ∧ ∀ e : ℤ, (∀ a ∈ as, e ∣ a) → e ∣ (d:ℤ) + +/-- Proposition 1.6.1 (Goodman, Algebra: Abstract and Concrete). Addition and multiplication on the integers are commutative and associative, 0 and 1 are their respective identities, the distributive law holds, and a product of integers is nonzero iff both factors are nonzero. ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_1 : ∀ (a b c : ℤ), (a + b = b + a) ∧ (a + (b + c) = (a + b) + c) ∧ (0 + a = a) ∧ (a + (-a) = 0) ∧ (a * b = b * a) ∧ (a * (b * c) = (a * b) * c) ∧ (1 * a = a) ∧ (a * (b + c) = a * b + a * c) ∧ (∀ (x y : ℤ), x * y ≠ 0 → x ≠ 0 ∧ y ≠ 0) + +/-- Proposition 1.6.4 (Goodman, Algebra: Abstract and Concrete). Any natural number greater than 1 can be written as a product of prime numbers. ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_4 : ∀ (n : ℕ), n > 1 → ∃ (p : ℕ) (h : Nat.Prime p), p ∣ n + +/-- Theorem 1.6.6 (Goodman, Algebra: Abstract and Concrete). There are infinitely many prime numbers. ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_6 : ∃ (p : ℕ → ℕ), ∀ (n : ℕ), Nat.Prime (p n) ∧ ∀ (i j : ℕ), i ≠ j → p i ≠ p j + +/-- Proposition 1.6.7 (Goodman, Algebra: Abstract and Concrete). Given integers a and d with d ≥ 1, there exist unique integers q and r such that a = qd + r and 0 ≤ r < d. ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_7 : ∀ (a d : ℤ), d ≥ 1 → ∃! qr : ℤ × ℤ, a = qr.1 * d + qr.2 ∧ 0 ≤ qr.2 ∧ qr.2 < d + +/-- Proposition 1.6.9 (Goodman, Algebra: Abstract and Concrete). I(m,n) = {am+bn} is closed under addition and negation, absorbs multiplication by any integer, and any common divisor of m and n divides every element of I(m,n). ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_9 : ∀ (m n : ℤ), let I := {v : ℤ | ∃ a b : ℤ, v = a * m + b * n}; (∀ x ∈ I, ∀ y ∈ I, x + y ∈ I) ∧ (∀ x ∈ I, -x ∈ I) ∧ (∀ x : ℤ, ∀ z ∈ I, x * z ∈ I) ∧ (∀ b : ℤ, b ∣ m ∧ b ∣ n → ∀ z ∈ I, b ∣ z) + +/-- Lemma 1.6.10 (Goodman, Algebra: Abstract and Concrete). If a natural number d is a common divisor of m and n and an element of I(m, n), then d is the greatest common divisor of m and n. ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_10 : ∀ (m n d : ℤ), d ∣ m ∧ d ∣ n ∧ d ∈ {v : ℤ | ∃ a b : ℤ, v = a * m + b * n} → ∀ (x : ℤ), x ∣ m ∧ x ∣ n → x ∣ d + +/-- Proposition 1.6.11 (Goodman, Algebra: Abstract and Concrete). The natural number d, which is the greatest common divisor of the absolute values of m and n, is also the greatest common divisor of m and n, and d is an element of I(m, n). ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_11 : ∀ (m n : ℤ), m ≠ 0 ∧ n ≠ 0 → let d := Nat.gcd (Int.natAbs m) (Int.natAbs n); (d : ℤ) = Int.gcd m n ∧ (d : ℤ) ∈ {v : ℤ | ∃ a b : ℤ, v = a * m + b * n} + +/-- Corollary 1.6.13 (Goodman, Algebra: Abstract and Concrete). gcd(m,n) is the least positive element of I(m,n), and I(m,n) is exactly the set of integer multiples of gcd(m,n). ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_13 : ∀ (m n : ℤ), m ≠ 0 → n ≠ 0 → let I := {v : ℤ | ∃ a b : ℤ, v = a * m + b * n}; let d := Int.gcd m n; IsLeast {x : ℤ | 0 < x ∧ x ∈ I} (d : ℤ) ∧ I = {v : ℤ | ∃ k : ℤ, v = k * d} + +/-- Corollary 1.6.15 (Goodman, Algebra: Abstract and Concrete). Two nonzero integers m and n are relatively prime if and only if there exist integers s and t such that sm + tn = 1. ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_15 : ∀ (m n : ℤ), m ≠ 0 ∧ n ≠ 0 → Int.gcd m n = 1 ↔ ∃ (s t : ℤ), s * m + t * n = 1 + +/-- Corollary 1.6.17 (Goodman, Algebra: Abstract and Concrete). If a and b are relatively prime natural numbers and both divide an integer x, then their product ab also divides x. ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_17 : ∀ (a b : ℕ) (x : ℤ), Nat.Coprime a b ∧ (a:ℤ) ∣ x ∧ (b:ℤ) ∣ x → (a:ℤ) * b ∣ x + +/-- Proposition 1.6.18 (Goodman, Algebra: Abstract and Concrete). If p is a prime number and a is any nonzero integer, then either p divides a or p and a are relatively prime. ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_18 : ∀ (p : ℕ) (a : ℤ), Nat.Prime p ∧ a ≠ 0 → (p:ℤ) ∣ a ∨ IsCoprime (p:ℤ) a + +/-- Proposition 1.6.19 (Goodman, Algebra: Abstract and Concrete). If p is a prime number and a and b are nonzero integers, and p divides the product ab, then p divides a or p divides b. ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_19 : ∀ (p : ℕ) (a b : ℤ), Nat.Prime p ∧ a ≠ 0 ∧ b ≠ 0 → (p:ℤ) ∣ a * b → (p:ℤ) ∣ a ∨ (p:ℤ) ∣ b + +/-- Corollary 1.6.20 (Goodman, Algebra: Abstract and Concrete). If a prime number p divides a product of nonzero integers, then p divides one of the factors. ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_20 : ∀ (p : ℕ) (as : List ℤ), Nat.Prime p → (∀ (a : ℤ), a ∈ as → a ≠ 0) → (p:ℤ) ∣ List.prod as → ∃ (a : ℤ), a ∈ as ∧ (p:ℤ) ∣ a + +/-- Theorem 1.6.21 (Goodman, Algebra: Abstract and Concrete). The prime factorization of a natural number is unique. ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_21 : ∀ (n : ℕ), n > 1 → ∃! (ps : List ℕ), (∀ (p : ℕ), p ∈ ps → Nat.Prime p) ∧ n = List.prod ps + +/-- Lemma 1.6.23 (Goodman, Algebra: Abstract and Concrete). Given n >= 2 nonzero integers a_1..a_n, there is a natural number d and a unimodular (det a unit, i.e. det = +-1) integer n-by-n matrix Q such that the row vector a times Q equals (d, 0, ..., 0). ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_23 : ∀ (n : ℕ) (a : Fin n → ℤ), 2 ≤ n → (∀ i, a i ≠ 0) → ∃ (d : ℕ) (Q : Matrix (Fin n) (Fin n) ℤ), IsUnit Q.det ∧ ∀ j : Fin n, Matrix.vecMul a Q j = if j.val = 0 then (d : ℤ) else 0 + +/-- Proposition 1.6.24 (Goodman, Algebra: Abstract and Concrete). The greatest common divisor of a list of at least two nonzero integers exists and is an integer linear combination of the integers in the list. ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_24 : ∀ (as : List ℤ), as.length ≥ 2 → (∀ (a : ℤ), a ∈ as → a ≠ 0) → ∃ (d : ℕ) (cs : List ℤ), IsGCDOfList d as ∧ (d:ℤ) = List.sum (List.zipWith (· * ·) cs as) + +/-- Lemma 1.6.26 (Goodman, Algebra: Abstract and Concrete). If a list of integers is pairwise relatively prime and each integer in the list divides an integer z, then the product of the integers in the list also divides z. ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_26 : ∀ (as : List ℤ) (z : ℤ), as.length ≥ 2 → (∀ (i j : ℕ), i ≠ j → i < as.length → j < as.length → IsCoprime (as[i]) (as[j])) → (∀ (a : ℤ), a ∈ as → a ≠ 0) → (∀ (a : ℤ), a ∈ as → a ∣ z) → List.prod as ∣ z + +/-- Proposition 1.6.2 (Goodman, Algebra: Abstract and Concrete). If two integers multiply to 1, both are 1 or both are -1. ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_2_a : ∀ (u v : ℤ), u * v = 1 → (u = 1 ∧ v = 1) ∨ (u = -1 ∧ v = -1) + +/-- Proposition 1.6.2 (Goodman, Algebra: Abstract and Concrete). If two integers divide each other, they are equal or negatives of each other. ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_2_b : ∀ (a b : ℤ), a ∣ b ∧ b ∣ a → a = b ∨ a = -b + +/-- Proposition 1.6.2 (Goodman, Algebra: Abstract and Concrete). Divisibility of integers is transitive. ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_2_c : ∀ (a b c : ℤ), a ∣ b ∧ b ∣ c → a ∣ c + +/-- Proposition 1.6.2 (Goodman, Algebra: Abstract and Concrete). If an integer divides two others, it divides any integer linear combination of them. ASSERTED from the textbook, not proven here. -/ +axiom goodman_1_6_2_d : ∀ (a b c s t : ℤ), a ∣ b ∧ a ∣ c → a ∣ (s * b + t * c) + diff --git a/tests/test_build_database.py b/tests/test_build_database.py new file mode 100644 index 0000000..3f8b4c3 --- /dev/null +++ b/tests/test_build_database.py @@ -0,0 +1,69 @@ +import unittest + +from textbook.build_database import build, decl_name, split_prelude, statement_identifiers + +ENTRIES = [ + {"id": "goodman-1-6-1", "source_label": "Proposition 1.6.1", "kind": "proposition", + "statement": "\u2200 (a : \u2124), a + 0 = a", "prelude": "import Mathlib", + "natural_language": "Zero is an additive identity. [fix note: irrelevant]", + "requires": ["Int.add_zero"], "elaborates": True}, + {"id": "goodman-1-6-24", "source_label": "Proposition 1.6.24", "kind": "proposition", + "statement": "\u2200 (as : List \u2124), IsGCDOfList 1 as", "prelude": "import Mathlib\ndef IsGCDOfList (d : \u2115) (as : List \u2124) : Prop := True", + "natural_language": "", "requires": [], "elaborates": True}, + {"id": "goodman-1-6-99", "source_label": "Proposition 1.6.99", "kind": "proposition", + "statement": "\u2200 (as : List \u2124), IsGCDOfList 2 as", "prelude": "import Mathlib\ndef IsGCDOfList (d : \u2115) (as : List \u2124) : Prop := True", + "natural_language": "", "requires": [], "elaborates": True}, +] + + +class BuildDatabaseTests(unittest.TestCase): + def test_decl_name_is_a_legal_lean_identifier(self): + self.assertEqual(decl_name('goodman-1-6-2-a'), 'goodman_1_6_2_a') + + def test_split_prelude_separates_imports_from_defs(self): + imports, other = split_prelude('import Mathlib\ndef Foo := True') + self.assertEqual(imports, ['import Mathlib']) + self.assertEqual(other, 'def Foo := True') + + def test_unproven_entries_become_axioms(self): + text, index, emitted, skipped = build(ENTRIES) + self.assertIn('axiom goodman_1_6_1 :', text) + self.assertEqual(len(emitted), 3) + self.assertEqual(skipped, []) + self.assertTrue(all(r['status'] == 'asserted' for r in index)) + + def test_proven_entries_become_real_theorems_with_their_proof(self): + results = {"goodman-1-6-1": {"id": "goodman-1-6-1", "success": True, + "attempts": [{"proof": "simp"}]}} + text, index, _emitted, _skipped = build(ENTRIES, results) + self.assertIn('theorem goodman_1_6_1 :', text) + self.assertNotIn('axiom goodman_1_6_1 :', text) + self.assertIn(' simp', text) + statuses = {r['id']: r['status'] for r in index} + self.assertEqual(statuses['goodman-1-6-1'], 'proved') + self.assertEqual(statuses['goodman-1-6-24'], 'asserted') + + def test_shared_def_in_prelude_is_emitted_once_not_per_entry(self): + # Two entries share the same `def`; declaring it twice in one Lean file is an + # "already declared" error, so it must be hoisted and deduplicated. + text, _index, _emitted, _skipped = build(ENTRIES) + self.assertEqual(text.count('def IsGCDOfList'), 1) + self.assertEqual(text.count('import Mathlib'), 1) + + def test_require_checked_skips_unverified_entries(self): + entries = [dict(ENTRIES[0]), dict(ENTRIES[1], elaborates=False)] + _text, index, emitted, skipped = build(entries, require_checked=True) + self.assertEqual(emitted, ['goodman-1-6-1']) + self.assertEqual(skipped, ['goodman-1-6-24']) + self.assertEqual(len(index), 1) + + def test_index_carries_identifiers_and_strips_fix_notes(self): + _text, index, _emitted, _skipped = build(ENTRIES) + first = index[0] + self.assertIn('Int.add_zero', first['requires']) + self.assertNotIn('fix note', first['natural_language']) + self.assertNotIn('let', statement_identifiers('let x := 1')) + + +if __name__ == '__main__': + unittest.main() diff --git a/tests/test_search_database.py b/tests/test_search_database.py new file mode 100644 index 0000000..4fdc5dd --- /dev/null +++ b/tests/test_search_database.py @@ -0,0 +1,58 @@ +import unittest + +from textbook.search_database import format_for_prompt, search, tokenize + +INDEX = [ + {"name": "goodman_1_6_20", "id": "goodman-1-6-20", "source_label": "Corollary 1.6.20", + "kind": "corollary", "status": "asserted", + "statement": "\u2200 (p : \u2115) (as : List \u2124), Nat.Prime p \u2192 (p:\u2124) \u2223 List.prod as \u2192 \u2203 a \u2208 as, (p:\u2124) \u2223 a", + "natural_language": "", "identifiers": ["Nat.Prime", "List.prod"], "requires": ["Nat.Prime"]}, + {"name": "goodman_1_6_24", "id": "goodman-1-6-24", "source_label": "Proposition 1.6.24", + "kind": "proposition", "status": "asserted", + "statement": "\u2200 (as : List \u2124), \u2203 d, IsGCDOfList d as", + "natural_language": "", "identifiers": ["IsGCDOfList"], "requires": []}, + {"name": "goodman_1_6_1", "id": "goodman-1-6-1", "source_label": "Proposition 1.6.1", + "kind": "proposition", "status": "asserted", + "statement": "\u2200 (a : \u2124), a + 0 = a", "natural_language": "", + "identifiers": [], "requires": []}, +] + + +class SearchDatabaseTests(unittest.TestCase): + def test_tokenize_keeps_qualified_names_and_drops_stopwords(self): + tokens = tokenize('let x := Nat.Prime p') + self.assertIn('Nat.Prime', tokens) + self.assertNotIn('let', tokens) + + def test_exact_premise_ranks_first(self): + hits = search(INDEX, '\u22a2 IsGCDOfList d as', limit=3) + self.assertEqual(hits[0]['name'], 'goodman_1_6_24') + + def test_rare_identifier_outweighs_common_one(self): + # Both premises mention List; only one mentions Nat.Prime, so the goal about + # primes must prefer it rather than tying on the common token. + hits = search(INDEX, '\u22a2 Nat.Prime p \u2192 (p:\u2124) \u2223 List.prod as', limit=3) + self.assertEqual(hits[0]['name'], 'goodman_1_6_20') + + def test_irrelevant_premises_are_dropped_not_ranked_last(self): + hits = search(INDEX, '\u22a2 IsGCDOfList d as', limit=5) + self.assertNotIn('goodman_1_6_1', [h['name'] for h in hits]) + + def test_proven_premise_is_preferred_over_an_asserted_one(self): + index = [dict(INDEX[1]), dict(INDEX[1], name='proved_twin', id='proved-twin', + status='proved', source_label='Proposition 1.6.24b')] + hits = search(index, '\u22a2 IsGCDOfList d as', limit=2) + self.assertEqual(hits[0]['name'], 'proved_twin') + + def test_limit_is_respected_and_empty_result_is_explained(self): + self.assertEqual(len(search(INDEX, '\u22a2 List.prod as', limit=1)), 1) + self.assertIn('no database premise', format_for_prompt([])) + + def test_format_for_prompt_marks_axioms_distinctly(self): + text = format_for_prompt(search(INDEX, '\u22a2 IsGCDOfList d as', limit=1)) + self.assertIn('asserted from the book (axiom)', text) + self.assertIn('goodman_1_6_24', text) + + +if __name__ == '__main__': + unittest.main() diff --git a/textbook/README.md b/textbook/README.md index 97c6a66..65bbb73 100644 --- a/textbook/README.md +++ b/textbook/README.md @@ -6,23 +6,35 @@ distinct things `lean-bench`/`lean-agent` can use, not one: - **The bench** (`datasets/goodman-1.6-exercises.jsonl`): real problems the reader is meant to solve, sourced from the book's own **Exercises** at the end of each section. These are the actual targets `lean-bench` scores an agent against. -- **The library candidates** (`library_candidates/goodman-1.6.jsonl`): the book's - stated Theorem/Proposition/Lemma/Corollary claims from the section's main text. - These are NOT bench targets -- they are premises waiting to be proven once and - then reused, the way Mathlib itself is a library of already-proven facts an agent - can cite while proving something new. An entry only belongs in the trustworthy, - reusable library after `lean-bench` has actually proven it for real (see step 5); - `build_library.py` already enforces this -- it only assembles entries whose - `results.jsonl` says `success: true`, with the exact proof that was checked, never - anything from this file directly. -- **Definitions** (`textbook/*.definitions.json` + `lib/Definitions.lean`): a - concept a bench/library statement depends on. When Mathlib already has it - (`mathlib_ref` set), statements just use that name directly. When it doesn't - (`mathlib_ref: null`), the manifest also carries real, hand-written Lean code - (`lean_code`), compiled by `build_definitions.py` into an actual importable - `.lean` file -- Lean can only ever verify a proof about a concept that exists as - real Lean code somewhere, a JSON description of a definition is not enough for it - to typecheck anything that mentions it. +- **The database** (`database/goodman-1.6.jsonl` -> `lib/Goodman/Chapter01Section06.lean` + + `database/goodman-1.6.index.jsonl`): the book's stated Theorem/Proposition/ + Lemma/Corollary claims from the main text, turned by `build_database.py` into real + Lean declarations an agent can **cite by name** while proving a bench target -- + the "third party math library" role Mathlib plays, except scoped to this book. + You do not re-prove Mathlib's theorems to use them, and the same applies here: the + book proves its own body results, and its exercises are posed assuming them. So an + entry is emitted as an `axiom` (asserted from the textbook) until a real + `lean-bench` run proves it, at which point `--results` upgrades it to a + `theorem` carrying the exact proof that was verified. + + The cost of that shortcut is real and worth stating plainly: anything proven + *through* an axiom inherits it, so a garbled extraction asserted as an axiom can + make downstream "proofs" worthless. Two guards: `--require-checked` refuses any + entry that hasn't passed `check_statements.py`, and the verifier's + `#print axioms` check surfaces what a finished proof actually rests on. Every + axiom here still needs a human to have read it against the book. +- **Retrieval** (`search_database.py`): given the current goal, ranks database + premises by identifier/symbol overlap with rare identifiers weighted higher, and + formats the top few for the LLM prompt. This is the step the proof loop calls at + each line -- it narrows ~20 premises to the few worth showing, and cannot tell you + whether one applies; only Lean can. Swapping in embeddings later means replacing + `score_premise()` and nothing else. +- **Definitions** (`textbook/*.definitions.json` + `lib/Definitions.lean`): a concept + a statement depends on. When Mathlib has it (`mathlib_ref` set), statements use + that name directly. When it doesn't (`mathlib_ref: null`), the manifest carries + real hand-written Lean (`lean_code`), compiled by `build_definitions.py` into an + importable `.lean` file -- Lean can only verify a proof about a concept that + exists as real Lean code, a JSON description of a definition is not enough. This pipeline does not itself prove anything or run Lean; see "What this pipeline does not do" below and `lean-agent`'s own README for how proving actually happens @@ -88,7 +100,7 @@ export DASHSCOPE_API_KEY=... # or put it in lean-bench/.env (gitignored) python3 textbook/formalize.py \ textbook/section_1_6.txt textbook/section_1_6.index.json \ --model qwen-max --base-url https://dashscope.aliyuncs.com/compatible-mode/v1 \ - --out-dataset library_candidates/goodman-1.6.jsonl \ + --out-dataset database/goodman-1.6.jsonl \ --out-definitions textbook/goodman-1.6.definitions.json \ --out-excluded textbook/goodman-1.6.excluded.jsonl @@ -121,7 +133,7 @@ mis-included as an unconditional theorem). ### 4. Check candidate statements type-check on your machine ```sh -python3 textbook/check_statements.py library_candidates/goodman-1.6.jsonl \ +python3 textbook/check_statements.py database/goodman-1.6.jsonl \ --lean-project /path/to/your/mathlib-project \ --lean-command '["lake","env","lean"]' \ --report textbook/goodman-1.6.elab-report.jsonl @@ -157,19 +169,28 @@ task, matching how `check_statements.py` elaborates one task at a time), so `lib/Definitions.lean` is the single canonical copy and the inlined ones must stay in sync with it by construction (generated from the same manifest). -### 7. Assemble proven library candidates into a reusable library file +### 7. Generate the citable premise database ```sh -python3 textbook/build_library.py library_candidates/goodman-1.6.jsonl \ - results/goodman-1.6-001-library/results.jsonl --out lib/Chapter01Section06.lean +python3 textbook/build_database.py database/goodman-1.6.jsonl \ + --out-lean lib/Goodman/Chapter01Section06.lean \ + --out-index database/goodman-1.6.index.jsonl \ + --require-checked ``` -(This step needs its own `lean-bench` run over `library_candidates/`, proving those -statements the same way step 5 proves the exercises -- not yet done for section -1.6.) Only entries that were actually proven in that run go in, with the exact -proof that was checked, verbatim. Later chapters `import` this file to build on -already-proven results -- it's one flat `.lean` file, not a real Lake -package/module boundary. +Add `--results results/goodman-1.6-library-001/results.jsonl` once a `lean-bench` +run over `database/goodman-1.6.jsonl` has proven some of them, to upgrade those +entries from `axiom` to real theorems. Then query it with the current goal: + +```sh +python3 textbook/search_database.py database/goodman-1.6.index.jsonl \ + "\u22a2 Nat.Prime p \u2192 (p:\u2124) \u2223 List.prod as \u2192 \u2203 a \u2208 as, (p:\u2124) \u2223 a" +``` + +(`build_library.py` predates this and remains for the narrower job of assembling +*only* proven entries with no axioms at all; note it attaches each entry's +non-import prelude per-theorem, which would emit a shared `def` twice in one file -- +`build_database.py` hoists and dedupes them instead.) ## How this is meant to connect to lean-agent diff --git a/textbook/build_database.py b/textbook/build_database.py new file mode 100644 index 0000000..0ced177 --- /dev/null +++ b/textbook/build_database.py @@ -0,0 +1,164 @@ +"""Generate the citable premise database from a book section's main-content statements. + +This is the "third party math library" half of the pipeline: the book's own +Theorem/Proposition/Lemma/Corollary claims, turned into real Lean declarations that +lean-agent can cite by name while proving something else (the bench targets, which +come from the exercises instead -- see formalize_exercises.py). + +Two outputs: + +1. An importable Lean file where every database entry is a named declaration. An + entry is emitted as a real `theorem ... := by ` when a lean-bench run has + actually proven it (status "proved"), and otherwise as an `axiom` -- asserted from + the textbook, which is what the book itself does for its own body results before + an exercise asks you to use them. This is deliberate and has a real cost: anything + proven *through* an axiom inherits it, which is exactly why the verifier's + `#print axioms` check matters. A statement that only elaborates is not the same as + a statement that is true, and a garbled extraction asserted as an axiom can make + downstream "proofs" worthless -- so every axiom here needs to have been read by a + human against the book, and `--require-checked` refuses to emit any entry not + marked as having passed check_statements.py. + +2. A search index (JSONL) carrying each entry's declaration name, statement, the + Mathlib identifiers it mentions, and its status -- what search_database.py ranks + against the current goals at each step of a proof. + +Pass a lean-bench run's results.jsonl with --results to upgrade the entries it +proved from axiom to a real theorem carrying the exact proof that run verified. +""" +import argparse +import json +import re +from pathlib import Path + +IDENT_RE = re.compile(r'[A-Za-z_][A-Za-z0-9_]*(?:\.[A-Za-z_][A-Za-z0-9_]*)+|[A-Za-z_][A-Za-z0-9_]*') +# Tokens that say nothing about which premise is relevant. +STOPWORDS = {'let', 'in', 'fun', 'if', 'then', 'else', 'true', 'false', 'Prop', 'Type'} + + +def load_jsonl(path): + return [json.loads(line) for line in path.read_text(encoding='utf-8').splitlines() if line.strip()] + + +def decl_name(entry_id): + """goodman-1-6-2-a -> goodman_1_6_2_a (a legal Lean identifier).""" + return entry_id.replace('-', '_') + + +def split_prelude(prelude): + """Return (import lines, other prelude lines) for one entry's prelude.""" + imports, other = [], [] + for line in (prelude or '').splitlines(): + (imports if line.strip().startswith('import ') else other).append(line) + return imports, '\n'.join(other).strip() + + +def statement_identifiers(statement): + """Identifiers mentioned in a statement, for the search index.""" + found = [] + for match in IDENT_RE.findall(statement or ''): + if match in STOPWORDS or match in found or len(match) < 2: + continue + found.append(match) + return found + + +def build(entries, results=None, require_checked=False): + results = results or {} + + lines = ['-- Generated by textbook/build_database.py -- do not hand-edit.', + '-- Citable premise database from the textbook\'s main content.', + '-- `axiom` entries are asserted from the book, NOT proven here: anything', + '-- proven through one inherits it, so check `#print axioms` downstream.', + ''] + + shared_imports, shared_defs = [], [] + for entry in entries: + imports, other = split_prelude(entry.get('prelude')) + for line in imports: + if line.strip() not in shared_imports: + shared_imports.append(line.strip()) + # A def can only be declared once per file, so dedupe rather than attaching + # it per-theorem the way build_library.py does. + if other and other not in shared_defs: + shared_defs.append(other) + + lines.extend(sorted(shared_imports)) + lines.append('') + for block in shared_defs: + lines.append(block) + lines.append('') + + index, emitted, skipped = [], [], [] + for entry in entries: + entry_id = entry['id'] + if require_checked and not entry.get('elaborates'): + skipped.append(entry_id) + continue + + name = decl_name(entry_id) + result = results.get(entry_id) + proved = bool(result and result.get('success') and result.get('attempts')) + provenance = entry.get('source_label', entry_id) + + doc = f'/-- {provenance} (Goodman, Algebra: Abstract and Concrete).' + if entry.get('natural_language'): + doc += f' {entry["natural_language"].split("[fix note:")[0].strip()}' + doc += (' Proven by lean-bench.' if proved + else ' ASSERTED from the textbook, not proven here.') + ' -/' + lines.append(doc) + + if proved: + proof = result['attempts'][-1]['proof'] + lines.append(f'theorem {name} : {entry["statement"]} := by') + lines.extend(' ' + line for line in proof.splitlines()) + else: + lines.append(f'axiom {name} : {entry["statement"]}') + lines.append('') + + index.append({ + "name": name, + "id": entry_id, + "source_label": entry.get('source_label'), + "kind": entry.get('kind'), + "status": "proved" if proved else "asserted", + "statement": entry['statement'], + "natural_language": entry.get('natural_language', '').split('[fix note:')[0].strip(), + "identifiers": statement_identifiers(entry['statement']), + "requires": entry.get('requires', []), + }) + emitted.append(entry_id) + + return '\n'.join(lines), index, emitted, skipped + + +def main(): + parser = argparse.ArgumentParser(description='Generate the citable premise database from main-content statements') + parser.add_argument('database', type=Path, help='JSONL of main-content statements, e.g. database/goodman-1.6.jsonl') + parser.add_argument('--results', type=Path, help="a lean-bench run's results.jsonl; proven entries become real theorems") + parser.add_argument('--out-lean', type=Path, required=True, help='importable Lean file of citable premises') + parser.add_argument('--out-index', type=Path, required=True, help='JSONL search index for search_database.py') + parser.add_argument('--require-checked', action='store_true', + help='refuse entries not marked "elaborates": true (i.e. not yet verified by check_statements.py)') + args = parser.parse_args() + + entries = load_jsonl(args.database) + results = {r['id']: r for r in load_jsonl(args.results)} if args.results else None + text, index, emitted, skipped = build(entries, results, args.require_checked) + + args.out_lean.parent.mkdir(parents=True, exist_ok=True) + args.out_lean.write_text(text + '\n', encoding='utf-8') + args.out_index.parent.mkdir(parents=True, exist_ok=True) + with args.out_index.open('w', encoding='utf-8') as stream: + for record in index: + stream.write(json.dumps(record, ensure_ascii=False) + '\n') + + proved = sum(1 for r in index if r['status'] == 'proved') + print(f'{len(emitted)} premises -> {args.out_lean} ({proved} proven, {len(emitted) - proved} asserted as axioms)') + print(f'search index -> {args.out_index}') + if skipped: + print(f'{len(skipped)} skipped for not being elaboration-checked: {", ".join(skipped)}') + + +if __name__ == '__main__': + main() diff --git a/textbook/search_database.py b/textbook/search_database.py new file mode 100644 index 0000000..ddccace --- /dev/null +++ b/textbook/search_database.py @@ -0,0 +1,99 @@ +"""Rank premises from the database against the current proof goals. + +This is the retrieval step of the intended lean-agent loop: rather than asking the +LLM to prove a target in one shot, the agent keeps a list of open goals (the proof +state, as vscode-lean4 displays it), and at each step searches the premise database +for entries that might apply to the goal in front of it. The ranked results are what +gets shown to the LLM alongside the goal, so the next line of Lean it writes can +cite a real premise by name instead of inventing a lemma. + +Scoring here is deliberately simple and dependency-free: overlap of identifiers and +symbols between the goal and each premise, weighted so that a rare identifier +matters more than a common one (`IsGCDOfList` appearing in both is a much stronger +signal than `Int`), plus a small bonus for an already-proven premise over one merely +asserted as an axiom from the book. It is a ranking heuristic, not a decision +procedure: it narrows 20-odd premises to the few worth showing, and cannot tell you +whether a premise actually applies -- only Lean can. Swapping in embeddings later +means replacing score_premise() and nothing else. +""" +import argparse +import json +import math +import re +from collections import Counter +from pathlib import Path + +TOKEN_RE = re.compile(r'[A-Za-z_][A-Za-z0-9_]*(?:\.[A-Za-z_][A-Za-z0-9_]*)+|[A-Za-z_][A-Za-z0-9_]*|[∣∀∃↔→∧∨¬≤≥≠∈]') +STOPWORDS = {'let', 'in', 'fun', 'if', 'then', 'else', 'true', 'false', 'Prop', 'Type', 'this'} + + +def load_index(path): + return [json.loads(line) for line in path.read_text(encoding='utf-8').splitlines() if line.strip()] + + +def tokenize(text): + return [t for t in TOKEN_RE.findall(text or '') if t not in STOPWORDS and len(t) > 1] + + +def document_frequencies(index): + """How many premises each token appears in, for inverse-document-frequency weighting.""" + frequencies = Counter() + for record in index: + for token in set(tokenize(record['statement']) + record.get('identifiers', []) + + record.get('requires', [])): + frequencies[token] += 1 + return frequencies + + +def score_premise(goal_tokens, record, frequencies, total): + premise_tokens = set(tokenize(record['statement']) + record.get('identifiers', []) + + record.get('requires', [])) + score = 0.0 + for token in set(goal_tokens) & premise_tokens: + # Rare tokens are far more informative than ones every premise mentions. + score += math.log(1 + total / (1 + frequencies.get(token, 0))) + if record.get('status') == 'proved': + score *= 1.1 # prefer a real theorem over an axiom asserted from the book + return score + + +def search(index, goal, limit=5): + """Premises ranked against one goal, best first. Zero-score entries are dropped.""" + frequencies = document_frequencies(index) + total = max(len(index), 1) + goal_tokens = tokenize(goal) + scored = [] + for record in index: + score = score_premise(goal_tokens, record, frequencies, total) + if score > 0: + scored.append((score, record)) + scored.sort(key=lambda pair: (-pair[0], pair[1]['name'])) + return [{**record, "score": round(score, 3)} for score, record in scored[:limit]] + + +def format_for_prompt(hits): + """The premise list as it would be shown to the LLM next to the current goal.""" + if not hits: + return '(no database premise looks relevant to this goal)' + lines = [] + for hit in hits: + status = 'proven' if hit['status'] == 'proved' else 'asserted from the book (axiom)' + lines.append(f"{hit['name']} [{hit['source_label']}, {status}, score {hit['score']}]\n" + f" {hit['statement']}") + return '\n'.join(lines) + + +def main(): + parser = argparse.ArgumentParser(description='Rank database premises against a proof goal') + parser.add_argument('index', type=Path, help='search index from build_database.py') + parser.add_argument('goal', help='the current goal, as Lean prints it') + parser.add_argument('--limit', type=int, default=5) + parser.add_argument('--json', action='store_true', help='emit raw JSON instead of prompt text') + args = parser.parse_args() + + hits = search(load_index(args.index), args.goal, args.limit) + print(json.dumps(hits, ensure_ascii=False, indent=2) if args.json else format_for_prompt(hits)) + + +if __name__ == '__main__': + main()