From 04d827b3b36e81393ce8f9415a0aff4c5b30dd2c Mon Sep 17 00:00:00 2001 From: Claude Bot Date: Fri, 18 Sep 2026 19:27:40 +0000 Subject: [PATCH] Split pipeline into real bench (exercises) vs library candidates (body) Restructures the textbook pipeline around the distinction the body-derived dataset had been blurring: a bench should be actual unsolved problems, and a reusable premise library should only ever contain statements that have really been proven, the way Mathlib itself works. - library_candidates/goodman-1.6.jsonl (renamed from datasets/goodman-1.6.jsonl): the book's own Theorem/Proposition/Lemma/Corollary claims from the main text. Not bench targets -- premises waiting to be proven once via a real lean-bench run, then assembled into the reusable library by build_library.py (which already only keeps success:true entries with their checked proof, unchanged by this commit). - datasets/goodman-1.6-exercises.jsonl (new): the actual bench, sourced from the book's Exercises 1.6 block via two new scripts, textbook/extract_exercises.py (slices the Exercises block, lists its numbered items, drops a known false-positive class where a wrapped cross-reference like "...Proposition\n1.6.19." looks like a real exercise heading) and textbook/formalize_exercises.py (LLM step, given both the exercises and body text together since many exercises say "Prove Proposition N.N.N" instead of restating the claim). - Both formalize.py and formalize_exercises.py's validate() now enforce that every checklist item is covered by at least one output entry (included or explicitly excluded with a reason); formalize_exercises.py did not have this yet and a first real run silently dropped 7 of 15 checklist items with no trace before this was added. - All 12 model-produced exercise entries needed real fixes before commit, the same review pass applied to the body pilot: 3 exercises literally ask to prove an already-stated body claim (Exercise 1.6.1 -> Proposition 1.6.7, 1.6.2 -> Proposition 1.6.9, 1.6.7 -> Proposition 1.6.18, 1.6.9 -> Corollary 1.6.20, 1.6.15 -> Lemma 1.6.26) and now reuse that claim's own already-checked statement verbatim instead of an independently re-derived (and in one case strictly weaker) restatement; two entries (1.6.2, 1.6.11) had literal math prose like "I(m, n)" or "gcd(n1,...,nk)" leaked into the statement field, which is not valid Lean; several had untyped/ambiguous gcd or Prime usage fixed the same way the earlier body fixes were (Nat.Prime, IsCoprime, explicit casts, IsGreatest instead of max on a Set); and Exercise 1.6.12 part (a) turned out to be a discussion question whose unconditional-identity reading is actually false (6, 10, 15 are jointly coprime but not pairwise coprime), so it was moved to the excluded file with a reason instead of committed as a false theorem. - Definitions can now be real, compiled Lean, not only JSON metadata: Definition 1.6.22 (gcd of a list of integers, previously a null placeholder since no single Mathlib constant matches it) now has a real hand-written `def IsGCDOfList`, and textbook/build_definitions.py compiles any manifest's non-null lean_code entries into lib/Definitions.lean. goodman-1-6-24 (library) and the new goodman-1-6-ex-11-b/c, goodman-1-6-ex-12 (bench) all now use IsGCDOfList instead of repeating an inline existential. - textbook/README.md rewritten around the two-track design and records how this is meant to connect to lean-agent's eventual goal-directed proof search against the growing library (not yet built). - New tests for extract_exercises.py and build_definitions.py; full local suite still green (18/19, the one failure is the pre-existing, unrelated lean_agent import error in test_dataset.py). Co-Authored-By: Claude Sonnet 5 Claude-Session: https://claude.ai/code/session_017vbLFFJiHSZqGZHEkjvG5x --- .gitignore | 1 + README.md | 17 +- datasets/goodman-1.6-exercises.jsonl | 14 ++ lib/Definitions.lean | 11 + .../goodman-1.6.jsonl | 2 +- tests/test_build_definitions.py | 46 ++++ tests/test_extract_exercises.py | 49 ++++ textbook/README.md | 232 ++++++++++++------ textbook/build_definitions.py | 55 +++++ textbook/exercises_1_6.index.json | 62 +++++ textbook/extract_exercises.py | 101 ++++++++ textbook/formalize_exercises.py | 185 ++++++++++++++ textbook/goodman-1.6-exercises.excluded.jsonl | 4 + textbook/goodman-1.6.definitions.json | 4 +- 14 files changed, 702 insertions(+), 81 deletions(-) create mode 100644 datasets/goodman-1.6-exercises.jsonl create mode 100644 lib/Definitions.lean rename {datasets => library_candidates}/goodman-1.6.jsonl (94%) create mode 100644 tests/test_build_definitions.py create mode 100644 tests/test_extract_exercises.py create mode 100644 textbook/build_definitions.py create mode 100644 textbook/exercises_1_6.index.json create mode 100644 textbook/extract_exercises.py create mode 100644 textbook/formalize_exercises.py create mode 100644 textbook/goodman-1.6-exercises.excluded.jsonl diff --git a/.gitignore b/.gitignore index 03a9c1c..ff9fae4 100644 --- a/.gitignore +++ b/.gitignore @@ -9,3 +9,4 @@ results/ *.pdf textbook/*.txt textbook/*_raw.txt +.DS_Store diff --git a/README.md b/README.md index e55cb85..02f4187 100644 --- a/README.md +++ b/README.md @@ -29,11 +29,16 @@ mock 返回固定证明，仍由真实 Lean 检查。真实 LLM 需配置 endpoi ## 教科书形式化流水线 -`textbook/` 下有一套从教材 PDF 生成 lean-bench 数据集的工具（LLM 辅助抽取 -Theorem/Proposition/Lemma/Corollary，配 Definition 清单，事后把证出来的结果 -组装成可复用的 Lean 库文件），用法见 [textbook/README.md](textbook/README.md)。 +`textbook/` 下有一套从教材 PDF 生成两类数据的工具：真正的 bench 目标（来自每节 +的 Exercises，`datasets/`）和候选库（来自正文 Theorem/Proposition/Lemma/ +Corollary，`library_candidates/`，只有被真正证明过之后才进最终的可复用 Lean 库 +文件），配 Definition 清单（Mathlib 没有的概念会编译成真正可导入的 Lean 代码， +`lib/Definitions.lean`，不只是 JSON 元数据）。用法见 +[textbook/README.md](textbook/README.md)。 -## 状态数据集进度（更新于 2026-09-18） +## 状态（更新于 2026-09-18） -goodman-1.6.jsonl 全部 21 条 statement 已通过本地 Lean elaboration 检查 -（`check_statements.py`），定义清单中的幻觉 Mathlib 引用也已修正。 +`library_candidates/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/datasets/goodman-1.6-exercises.jsonl b/datasets/goodman-1.6-exercises.jsonl new file mode 100644 index 0000000..4ff79b0 --- /dev/null +++ b/datasets/goodman-1.6-exercises.jsonl @@ -0,0 +1,14 @@ +{"id": "goodman-1-6-ex-1", "source_label": "Exercise 1.6.1", "kind": "exercise", "statement": "∀ (a d : ℤ), d ≥ 1 → ∃! qr : ℤ × ℤ, a = qr.1 * d + qr.2 ∧ 0 ≤ qr.2 ∧ qr.2 < d", "prelude": "import Mathlib.Data.Int.Basic", "natural_language": "For all integers a and d, with d ≥ 1, there exist unique integers q and r such that a = qd + r and 0 ≤ r < d. [fix note: Exercise 1.6.1 literally asks to complete the proof of Proposition 1.6.7 via well-ordering; reused Proposition 1.6.7's own (already elaboration-checked) statement verbatim instead of re-deriving a weaker one -- the model's first draft dropped the uniqueness clause (`∃` instead of `∃!`), which is a materially different, weaker claim.]", "requires": ["Mathlib.Data.Int.Basic"], "references": ["Proposition 1.6.7"], "include_in_bench": true, "exclude_reason": null} +{"id": "goodman-1-6-ex-2", "source_label": "Exercise 1.6.2", "kind": "exercise", "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.Data.Int.Basic", "natural_language": "For integers m and n, the set I(m, n) has the properties: (a) For x, y in I(m, n), x + y and -x are in I(m, n). (b) For all x in Z, xI(m, n) is a subset of I(m, n). (c) If b divides m and n, then b divides all elements of I(m, n). [fix note: Exercise 1.6.2 literally asks to prove Proposition 1.6.9; reused Proposition 1.6.9's own statement verbatim. The model's first draft used bare `I(m, n)` as if it were a function call, which is not valid Lean -- there is no such function.]", "requires": ["Mathlib.Data.Int.Basic"], "references": ["Proposition 1.6.9"], "include_in_bench": true, "exclude_reason": null} +{"id": "goodman-1-6-ex-3", "source_label": "Exercise 1.6.3", "kind": "exercise", "statement": "∀ (p : ℕ), p > 1 → (∀ (a b : ℤ), a ≠ 0 → b ≠ 0 → (p:ℤ) ∣ (a * b) → ((p:ℤ) ∣ a ∨ (p:ℤ) ∣ b)) → Nat.Prime p", "prelude": "import Mathlib.Data.Nat.Prime", "natural_language": "If a natural number p > 1 has the property that for all nonzero integers a and b, if p divides the product ab, then p divides a or p divides b, then p is prime. [fix note: Fixed two type mismatches: bare `Prime p` (ambiguous which typeclass instance) changed to `Nat.Prime p` to match convention elsewhere; and `p ∣ (a * b)` for `p : ℕ`, `a b : ℤ` needed an explicit `(p:ℤ)` cast, same class of bug as the earlier library fixes.]", "requires": ["Mathlib.Data.Nat.Prime"], "references": [], "include_in_bench": true, "exclude_reason": null} +{"id": "goodman-1-6-ex-5", "source_label": "Exercise 1.6.5", "kind": "exercise", "statement": "∀ (m n : ℤ), m ≠ 0 → n ≠ 0 → Int.gcd m n = Int.gcd (|m|) (|n|)", "prelude": "import Mathlib.Data.Int.GCD", "natural_language": "For nonzero integers m and n, the greatest common divisor of m and n is equal to the greatest common divisor of their absolute values. [fix note: Original used bare `gcd m n` with `m n : ℤ`, ambiguous between the generic `GCDMonoid.gcd` (returns ℤ) and `Int.gcd` (returns ℕ); switched to `Int.gcd` explicitly (returns ℕ, matches the rest of the dataset's convention for integer gcd).]", "requires": ["Mathlib.Data.Int.GCD"], "references": [], "include_in_bench": true, "exclude_reason": null} +{"id": "goodman-1-6-ex-6", "source_label": "Exercise 1.6.6", "kind": "exercise", "statement": "∀ (m n : ℤ), m ≠ 0 → n ≠ 0 → IsGreatest {d : ℕ | (d:ℤ) ∣ m ∧ (d:ℤ) ∣ n} (Int.gcd m n)", "prelude": "import Mathlib.Data.Int.GCD", "natural_language": "For nonzero integers m and n, the greatest common divisor of m and n is the largest natural number dividing both m and n. [fix note: Original wrote `gcd m n = max {d : ℕ | ...}`, but `max` is not a function on `Set` in Mathlib (same bug class as an earlier library fix that needed `IsLeast`); 'is the largest natural number dividing both' is `IsGreatest` on the set of common divisors.]", "requires": ["Mathlib.Data.Int.GCD"], "references": [], "include_in_bench": true, "exclude_reason": null} +{"id": "goodman-1-6-ex-7", "source_label": "Exercise 1.6.7", "kind": "exercise", "statement": "∀ (p : ℕ) (a : ℤ), Nat.Prime p ∧ a ≠ 0 → (p:ℤ) ∣ a ∨ IsCoprime (p:ℤ) a", "prelude": "import Mathlib.Data.Nat.Prime Mathlib.Data.Int.GCD", "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. [fix note: Exercise 1.6.7 is exactly Proposition 1.6.18's claim; reused Proposition 1.6.18's own statement verbatim rather than re-deriving (the model's draft had the same `Prime p` / untyped `gcd p a = 1` issues as Exercise 1.6.3).]", "requires": ["Mathlib.Data.Nat.Prime", "Mathlib.Data.Int.GCD"], "references": [], "include_in_bench": true, "exclude_reason": null} +{"id": "goodman-1-6-ex-8", "source_label": "Exercise 1.6.8", "kind": "exercise", "statement": "∀ (a b x : ℤ), IsCoprime a b → a ∣ (b * x) → a ∣ x", "prelude": "import Mathlib.Data.Int.GCD", "natural_language": "If a and b are relatively prime integers and x is an integer, then if a divides the product bx, a divides x. [fix note: Original wrote `gcd a b = 1`; switched to `IsCoprime a b` for consistency with how 'relatively prime' is formalized everywhere else in this dataset (Definition 1.6.14).]", "requires": ["Mathlib.Data.Int.GCD"], "references": [], "include_in_bench": true, "exclude_reason": null} +{"id": "goodman-1-6-ex-9", "source_label": "Exercise 1.6.9", "kind": "exercise", "statement": "∀ (p : ℕ) (as : List ℤ), Nat.Prime p → (∀ (a : ℤ), a ∈ as → a ≠ 0) → (p:ℤ) ∣ List.prod as → ∃ (a : ℤ), a ∈ as ∧ (p:ℤ) ∣ a", "prelude": "import Mathlib.Data.Nat.Prime", "natural_language": "If a prime number p divides a product a₁ * a₂ * ... * aₙ of nonzero integers, then p divides one of the factors. [fix note: Exercise 1.6.9 is exactly Corollary 1.6.20's claim; reused Corollary 1.6.20's own statement verbatim. The model's draft used invalid variadic-ellipsis notation (`a₁ a₂ ... aₙ`) that is not valid Lean syntax at all -- an indexed list is required, matching how the body handles the same claim.]", "requires": ["Mathlib.Data.Nat.Prime"], "references": ["Proposition 1.6.19"], "include_in_bench": true, "exclude_reason": null} +{"id": "goodman-1-6-ex-11-a", "source_label": "Exercise 1.6.11(a)", "kind": "exercise", "statement": "∀ (ns : List ℤ), let I := {v : ℤ | ∃ ms : List ℤ, ms.length = ns.length ∧ v = (List.zipWith (· * ·) ms ns).sum}; (∀ x ∈ I, ∀ y ∈ I, x + y ∈ I) ∧ (∀ x ∈ I, -x ∈ I) ∧ (∀ (c : ℤ), ∀ x ∈ I, c * x ∈ I)", "prelude": "import Mathlib", "natural_language": "For a list of nonzero integers n1..nk with I the set of integer combinations of them, I is closed under addition, negation, and scalar multiplication.", "requires": [], "references": [], "include_in_bench": true, "exclude_reason": null} +{"id": "goodman-1-6-ex-11-b", "source_label": "Exercise 1.6.11(b)", "kind": "exercise", "statement": "∀ (ns : List ℤ) (d : ℕ), IsGCDOfList d ns → IsLeast {v : ℤ | v ∈ {v : ℤ | ∃ ms : List ℤ, ms.length = ns.length ∧ v = (List.zipWith (· * ·) ms ns).sum} ∧ 0 < v} (d : ℤ)", "prelude": "import Mathlib\ndef IsGCDOfList (d : ℕ) (as : List ℤ) : Prop :=\n (∀ a ∈ as, (d:ℤ) ∣ a) ∧ ∀ e : ℤ, (∀ a ∈ as, e ∣ a) → e ∣ (d:ℤ)", "natural_language": "The gcd of n1..nk is the least positive element of I (the set of their integer combinations).", "requires": [], "references": [], "include_in_bench": true, "exclude_reason": null} +{"id": "goodman-1-6-ex-11-c", "source_label": "Exercise 1.6.11(c)", "kind": "exercise", "statement": "∀ (ns : List ℤ) (d : ℕ), IsGCDOfList d ns → {v : ℤ | ∃ ms : List ℤ, ms.length = ns.length ∧ v = (List.zipWith (· * ·) ms ns).sum} = {v : ℤ | (d:ℤ) ∣ v}", "prelude": "import Mathlib\ndef IsGCDOfList (d : ℕ) (as : List ℤ) : Prop :=\n (∀ a ∈ as, (d:ℤ) ∣ a) ∧ ∀ e : ℤ, (∀ a ∈ as, e ∣ a) → e ∣ (d:ℤ)", "natural_language": "I (the set of integer combinations of n1..nk) equals the set of multiples of their gcd d.", "requires": [], "references": [], "include_in_bench": true, "exclude_reason": null} +{"id": "goodman-1-6-ex-12", "source_label": "Exercise 1.6.12(b)", "kind": "exercise", "statement": "∀ (ns : List ℤ), (∃ d : ℕ, IsGCDOfList d ns ∧ d = 1) ↔ (1 : ℤ) ∈ {v : ℤ | ∃ ms : List ℤ, ms.length = ns.length ∧ v = (List.zipWith (· * ·) ms ns).sum}", "prelude": "import Mathlib\ndef IsGCDOfList (d : ℕ) (as : List ℤ) : Prop :=\n (∀ a ∈ as, (d:ℤ) ∣ a) ∧ ∀ e : ℤ, (∀ a ∈ as, e ∣ a) → e ∣ (d:ℤ)", "natural_language": "(a) Determine if the integers n₁, n₂, ..., nₖ are relatively prime if and only if they are pairwise relatively prime. (b) Show that n₁, n₂, ..., nₖ are relatively prime if and only if 1 ∈ I(n₁, n₂, ..., nₖ). [fix note: Part (a) ('is relatively prime the same as pairwise relatively prime?') is a discussion question, not a fixed claim to formalize -- and its unconditional-identity reading is actually FALSE in general (e.g. 6, 10, 15 are jointly coprime but not pairwise coprime), so it cannot be stated as an unconditional theorem. Moved to the excluded file with a reason. This entry keeps only part (b), the genuine 'relatively prime iff 1 in I' claim, rewritten with `ns : List ℤ` / `IsGCDOfList` instead of the model's invalid variadic `gcd(n₁, n₂, ..., nₖ)` and `I(n₁, ..., nₖ)` notation.]", "requires": ["Mathlib.Data.Int.GCD"], "references": [], "include_in_bench": true, "exclude_reason": null} +{"id": "goodman-1-6-ex-14", "source_label": "Exercise 1.6.14", "kind": "exercise", "statement": "∀ (m n : ℤ), m ≠ 0 → n ≠ 0 → (IsCoprime m n ↔ ∀ (p : ℕ), Nat.Prime p → (p:ℤ) ∣ m → ¬((p:ℤ) ∣ n))", "prelude": "import Mathlib.Data.Int.GCD Mathlib.Data.Nat.Prime", "natural_language": "Show that two nonzero integers are relatively prime if and only if they have no common prime factors. Use this to give a different proof of Corollary 1.6.17, relying on the uniqueness of the prime factorization of an integer. [fix note: Fixed the same `Prime p` / untyped `gcd m n = 1` / missing ℤ casts as the other exercises; used `IsCoprime m n` for consistency.]", "requires": ["Mathlib.Data.Int.GCD", "Mathlib.Data.Nat.Prime"], "references": ["Corollary 1.6.17"], "include_in_bench": true, "exclude_reason": null} +{"id": "goodman-1-6-ex-15", "source_label": "Exercise 1.6.15", "kind": "exercise", "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.Data.Int.GCD", "natural_language": "Let a₁, a₂, ..., aₙ be pairwise relatively prime integers, and let a = a₁ * a₂ * ... * aₙ. If an integer z is divisible by each aᵢ, then z is divisible by a. [fix note: Exercise 1.6.15 literally asks to prove Lemma 1.6.26; reused Lemma 1.6.26's own statement verbatim instead of the model's invalid variadic-ellipsis draft.]", "requires": ["Mathlib.Data.Int.GCD"], "references": ["Lemma 1.6.26"], "include_in_bench": true, "exclude_reason": null} diff --git a/lib/Definitions.lean b/lib/Definitions.lean new file mode 100644 index 0000000..141efef --- /dev/null +++ b/lib/Definitions.lean @@ -0,0 +1,11 @@ +-- Generated by textbook/build_definitions.py -- hand-written Lean +-- definitions for concepts with no Mathlib equivalent. Regenerate +-- from the definitions manifest(s) instead of hand-editing. + +import Mathlib + +-- Definition 1.6.22: greatest common divisor (gcd) of several integers +-- No single ready-made Mathlib constant for 'gcd of a `List ℤ`' matches the book's definition verbatim, so this concept gets a real, hand-written Lean `def` (see lean_code) instead of only a JSON pointer -- it is compiled into textbook/lib/Definitions.lean by build_definitions.py and inlined into any statement's `prelude` that needs it, so Lean can actually elaborate proofs that use it, not just read a description of it. +def IsGCDOfList (d : ℕ) (as : List ℤ) : Prop := + (∀ a ∈ as, (d:ℤ) ∣ a) ∧ ∀ e : ℤ, (∀ a ∈ as, e ∣ a) → e ∣ (d:ℤ) + diff --git a/datasets/goodman-1.6.jsonl b/library_candidates/goodman-1.6.jsonl similarity index 94% rename from datasets/goodman-1.6.jsonl rename to library_candidates/goodman-1.6.jsonl index 1270a81..055c7aa 100644 --- a/datasets/goodman-1.6.jsonl +++ b/library_candidates/goodman-1.6.jsonl @@ -13,7 +13,7 @@ {"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 ℤ), (∀ a ∈ as, (d:ℤ) ∣ a) ∧ (∀ (e : ℤ), (∀ a ∈ as, e ∣ a) → e ∣ (d:ℤ)) ∧ (d:ℤ) = List.sum (List.zipWith (· * ·) cs as)", "prelude": "import Mathlib", "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-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} diff --git a/tests/test_build_definitions.py b/tests/test_build_definitions.py new file mode 100644 index 0000000..aaae918 --- /dev/null +++ b/tests/test_build_definitions.py @@ -0,0 +1,46 @@ +import json +import tempfile +import unittest +from pathlib import Path + +from textbook.build_definitions import build + + +def write_json(path, data): + path.write_text(json.dumps(data), encoding='utf-8') + + +class BuildDefinitionsTests(unittest.TestCase): + def test_only_entries_with_lean_code_are_emitted(self): + with tempfile.TemporaryDirectory() as directory: + path = Path(directory) / 'defs.json' + write_json(path, [ + {"label": "Definition A", "concept": "has mathlib equivalent", + "mathlib_ref": "Nat.Prime", "lean_code": None, "notes": ""}, + {"label": "Definition B", "concept": "needs hand-written def", + "mathlib_ref": None, "lean_code": "def Foo (n : Nat) : Prop := n = n", + "notes": "some note"}, + ]) + text, emitted = build([path]) + self.assertEqual(emitted, 1) + self.assertIn('def Foo (n : Nat) : Prop := n = n', text) + self.assertIn('Definition B', text) + self.assertNotIn('Definition A', text) # has a Mathlib ref, nothing to assemble + + def test_multiple_manifests_are_concatenated(self): + with tempfile.TemporaryDirectory() as directory: + directory = Path(directory) + path1 = directory / 'defs1.json' + path2 = directory / 'defs2.json' + write_json(path1, [{"label": "D1", "concept": "c1", "mathlib_ref": None, + "lean_code": "def D1 := True", "notes": ""}]) + write_json(path2, [{"label": "D2", "concept": "c2", "mathlib_ref": None, + "lean_code": "def D2 := True", "notes": ""}]) + text, emitted = build([path1, path2]) + self.assertEqual(emitted, 2) + self.assertIn('def D1 := True', text) + self.assertIn('def D2 := True', text) + + +if __name__ == '__main__': + unittest.main() diff --git a/tests/test_extract_exercises.py b/tests/test_extract_exercises.py new file mode 100644 index 0000000..66b5516 --- /dev/null +++ b/tests/test_extract_exercises.py @@ -0,0 +1,49 @@ +import unittest +from textbook.extract_exercises import extract_exercises, numbered_items + +FIXTURE = """\ +1.6. Divisibility in the Integers +body text +Proof. Exercise 1.6.15. n + +Exercises 1.6 + +1.6.1. Complete the following sketch. + (a) part a text +1.6.2. Prove Proposition 1.6.9. +1.6.3. Suppose that a natural number p > 1 has some property. This is the +converse of Proposition +1.6.19. + +1.7. Modular Arithmetic +next section text +""" + + +class ExtractExercisesTests(unittest.TestCase): + def test_extract_exercises_slices_between_headings(self): + block = extract_exercises(FIXTURE, 'Exercises 1.6', '1.7. Modular Arithmetic') + self.assertIn('1.6.1. Complete', block) + self.assertNotIn('next section text', block) + + def test_extract_exercises_missing_heading_raises(self): + with self.assertRaises(ValueError): + extract_exercises(FIXTURE, 'Exercises 1.6', 'Exercises 9.9') + + def test_numbered_items_orders_and_dedupes(self): + block = extract_exercises(FIXTURE, 'Exercises 1.6', '1.7. Modular Arithmetic') + items, _dropped = numbered_items(block, '1.6.') + self.assertEqual([i['number'] for i in items], ['1.6.1', '1.6.2', '1.6.3']) + + def test_numbered_items_drops_wrapped_cross_reference(self): + # '1.6.19.' alone on its own line, right after a big jump from 1.6.3, with no + # text on the same line, is a wrapped cross-reference ("...Proposition\n1.6.19."), + # not a real exercise 16 numbers ahead of the last real one. + block = extract_exercises(FIXTURE, 'Exercises 1.6', '1.7. Modular Arithmetic') + items, dropped = numbered_items(block, '1.6.', max_gap=3) + self.assertNotIn('1.6.19', [i['number'] for i in items]) + self.assertEqual([d['number'] for d in dropped], ['1.6.19']) + + +if __name__ == '__main__': + unittest.main() diff --git a/textbook/README.md b/textbook/README.md index 76fd32e..97c6a66 100644 --- a/textbook/README.md +++ b/textbook/README.md @@ -1,35 +1,62 @@ # Textbook formalization pipeline -把一本教科书（目前是 Goodman, *Algebra: Abstract and Concrete*）里正文的 -Theorem/Proposition/Lemma/Corollary 转成 lean-bench 能跑的任务 JSONL，配套 -Definition 清单（优先复用 Mathlib，Mathlib 没有的才手写），再由 lean-agent 在 -一个真正带 Mathlib 的 Lean 项目里验证/证明。这条流水线本身不跑 Lean，也不联网 -以外没有第三方依赖。 +Turns one book (currently Goodman, *Algebra: Abstract and Concrete*) into two +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. -- 不产出证明。生成的只是**待证命题**（`statement` 字段），证明留给 - `lean-agent`/`lean-bench` 去跑。 -- 不在 Cowork 沙盒里验证 Lean 语句能不能通过类型检查——沙盒里没有装 - Lean/Lake/Mathlib（架构也不兼容：本机 `~/.elan` 下是 macOS 二进制，沙盒是 - Linux VM，跑不了），所以 `check_statements.py` 必须在你本机、且是一个已经 - `lake exe cache get` 过的 Mathlib 项目里跑，见下面"本机环境准备"。 -- 不会把教科书 PDF 或者大段原文提取结果提交进 git——`.gitignore` 里已经排除 - 了 `*.pdf` 和 `textbook/*.txt`，这些是版权内容，只应该留在你本机。只有代码、 - 生成的最终数据集（短的 Lean 语句 + 自己改写的简短英文释义）会进仓库。 +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 +(goal-directed proof search against the library, not a single-shot proof attempt -- +see "How this is meant to connect to lean-agent" at the end of this file). -## 用法 +## What this pipeline does not do -### 1. 从 PDF 提取一章的版式文本 +- Does not produce proofs. Every `statement` field is an unproven target; a Lean + `sorry` would technically "complete" it, which is exactly why proving is left to + `lean-agent`/`lean-bench`, not this pipeline. +- Does not verify Lean statements type-check inside the Cowork sandbox -- there is + no Lean/Lake/Mathlib there (also architecturally incompatible: your local + `~/.elan` has macOS binaries, the sandbox is a Linux VM). `check_statements.py` + must run on your machine against a Mathlib-backed Lean project; see "Local + environment setup" below. +- Does not commit the textbook PDF or large raw/derived full-text extraction dumps + to git -- `.gitignore` excludes `*.pdf` and `textbook/*.txt`, since that's + copyrighted material that should only ever live on your machine. Only code, the + generated JSON/JSONL datasets (short Lean statements + your own short English + glosses), and the compiled `Definitions.lean` go into git. + +## Usage + +### 1. Extract one chapter's layout text from the PDF ```sh -pdftotext -layout -f <起始pdf页码> -l <结束pdf页码> uiowa-algebra.pdf textbook/chapterNN_layout.txt +pdftotext -layout -f -l uiowa-algebra.pdf textbook/chapterNN_layout.txt ``` -页码用 `pdfinfo`/`pypdf` 先核对——书里印的页码和 PDF 物理页码不是一回事（前 -面有目录、序言）。 +Check page numbers with `pdfinfo`/`pypdf` first -- the book's printed page numbers +and the PDF's physical page numbers differ (front matter, table of contents). -### 2. 切出一个 section，列出带编号的条目清单 +### 2. Slice out a section's body and its exercises separately ```sh python3 textbook/extract_section.py textbook/chapterNN_layout.txt \ @@ -38,96 +65,157 @@ python3 textbook/extract_section.py textbook/chapterNN_layout.txt \ --section-prefix "1.6." \ --out-text textbook/section_1_6.txt \ --out-index textbook/section_1_6.index.json + +python3 textbook/extract_exercises.py textbook/chapterNN_layout.txt \ + --start-heading "Exercises 1.6" \ + --end-heading "1.7. Modular Arithmetic" \ + --section-prefix "1.6." \ + --out-text textbook/exercises_1_6.txt \ + --out-index textbook/exercises_1_6.index.json ``` -`--start-heading`/`--end-heading` 必须和版式文本里独占一行的章节标题**逐字** -一致（提取时打印出的书本身的标题行）；`--end-heading` 留空就切到文件末尾。 -输出的 index JSON 是这个 section 里所有 `Theorem/Proposition/Lemma/ -Corollary/Definition N.N.N` 开头的条目清单（自动去重了跨页重复的标签），用来 -让下一步的 LLM 不漏项、不编项目。 +Headings must match the layout text's own section-title lines **verbatim**. +`extract_exercises.py` drops obvious false positives (a sentence like "...converse +of Proposition\n1.6.19." can wrap so the bare number lands alone at a line start, +looking exactly like a real exercise heading) -- anything dropped is printed to +stderr, never silently lost. -### 3. 用 LLM 把 section 形式化成候选 Lean 语句 +### 3. Formalize the body (-> library candidates) and the exercises (-> bench) separately ```sh -export DASHSCOPE_API_KEY=... # 或者写进 lean-bench/.env（已 gitignore） +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 datasets/goodman-1.6.jsonl \ + --out-dataset library_candidates/goodman-1.6.jsonl \ --out-definitions textbook/goodman-1.6.definitions.json \ --out-excluded textbook/goodman-1.6.excluded.jsonl + +python3 textbook/formalize_exercises.py \ + textbook/section_1_6.txt textbook/exercises_1_6.txt textbook/exercises_1_6.index.json \ + --model qwen-max --base-url https://dashscope.aliyuncs.com/compatible-mode/v1 \ + --out-dataset datasets/goodman-1.6-exercises.jsonl \ + --out-excluded textbook/goodman-1.6-exercises.excluded.jsonl ``` -模型会为每条 Theorem/Proposition/Lemma/Corollary 产出一个 Lean 4 命题 -（`statement`）、需要的 `prelude`（通常就是 `import Mathlib`）、一句自己改写 -的英文释义，以及用到的 Mathlib 标识符列表；为每条相关的 Definition 产出一个 -清单条目——如果 Mathlib 已经有对应概念（`mathlib_ref` 非空）就不写 Lean 代 -码，只有 Mathlib 没有的概念才会给出手写的 `def`。判断这条目根本没法形式化 -（纯计算题、内容太模糊/被 PDF 提取污染到读不出原意）的条目，会带着 -`include_in_bench: false` 和原因单独写进 `--out-excluded`，不会进真正的数据 -集，但也不会被静默丢弃——都留痕方便你复核。 +`formalize_exercises.py` is given the body text too, because many exercises say +things like "Prove Proposition 1.6.9" instead of restating the claim -- the model +needs the body to know what that actually says, and is told to write out the full +claim, never a placeholder like "the statement of Proposition 1.6.9". -源 PDF 的数学符号提取质量很差（≡、∈、上下标经常丢失或乱码），这一步依赖模 -型自己对标准教材内容的知识去猜测/还原真实含义，**不是逐字翻译提取出来的文 -本**。所以生成的候选语句必须经过下一步验证，不能直接信。 +Both steps validate that every checklist item is covered by at least one output +entry (included or explicitly excluded with a reason) and raise an error if the +model silently drops one instead -- this caught a real bug during the exercises +pilot (7 of 15 checklist items were dropped with no trace on the first attempt). -### 4. 在你本机验证候选语句能不能通过类型检查 +The source PDF's math symbol extraction is unreliable (missing/garbled ≡, ∈, +superscripts), so this step leans on the model's own knowledge of standard textbook +mathematics rather than literal transcription. Candidate statements must go through +step 4 before you trust them -- in practice, even after that, expect to still need +to read and fix a meaningful fraction by hand (both the exercises and the original +body pilot needed real fixes to type mismatches, invalid syntax, and even one +mathematically false claim smuggled in as a "prove or disprove" exercise that got +mis-included as an unconditional theorem). -见下面"本机环境准备"先搭好一个带 Mathlib 的 Lake 项目，然后： +### 4. Check candidate statements type-check on your machine ```sh -python3 textbook/check_statements.py datasets/goodman-1.6.jsonl \ +python3 textbook/check_statements.py library_candidates/goodman-1.6.jsonl \ --lean-project /path/to/your/mathlib-project \ --lean-command '["lake","env","lean"]' \ --report textbook/goodman-1.6.elab-report.jsonl + +python3 textbook/check_statements.py datasets/goodman-1.6-exercises.jsonl \ + --lean-project /path/to/your/mathlib-project \ + --lean-command '["lake","env","lean"]' \ + --report textbook/goodman-1.6-exercises.elab-report.jsonl ``` -这一步只检查"这句 Lean 能不能通过类型检查"（用 `sorry` 占位），**不检查证明 -是否存在、也不检查是否忠实于原书**——分别对应两件不同的事：语法/引用是否正 -确，跟数学内容是否正确。失败的条目（`FAIL`）要么是模型编造了不存在的 -Mathlib 标识符，要么是语句本身写错了，需要你告诉我具体哪条、Lean 报的什么 -错，我再改。 +This only checks "does this Lean statement type-check" (via `sorry`), not "is it +provable" or "is it faithful to the book" -- report any `FAIL` id and its Lean +diagnostics and they'll get fixed and pushed back. -### 5. 用 lean-agent/lean-bench 真正证明 +### 5. Prove the bench targets for real with lean-agent/lean-bench ```sh -lean-bench datasets/goodman-1.6.jsonl --output results/goodman-1.6-001 \ +lean-bench datasets/goodman-1.6-exercises.jsonl --output results/goodman-1.6-001 \ --lean-project /path/to/your/mathlib-project --lean-command '["lake","env","lean"]' \ --model ... --base-url ... ``` -### 6. 把证出来的定理组装成一份可复用的库文件 +### 6. Compile hand-written definitions into real, importable Lean ```sh -python3 textbook/build_library.py datasets/goodman-1.6.jsonl \ - results/goodman-1.6-001/results.jsonl --out lib/Chapter01Section06.lean +python3 textbook/build_definitions.py textbook/goodman-1.6.definitions.json --out lib/Definitions.lean ``` -只有这次跑真的证出来的定理（`results.jsonl` 里 `success: true`）才会被收进 -去，直接复用验证时确认过的那个证明，不会引入新的证明风险。后续章节要用这些 -已证定理时，`import` 这份文件——注意这只是把已证结果攒成一个文件，不是一个真 -正的 Lake 包/模块边界。 +Only definitions with no Mathlib equivalent (`mathlib_ref: null`) contribute +anything here -- everything else is used directly by name. Any statement whose +`prelude` needs one of these also inlines the `def` itself (self-contained per +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). -## 本机环境准备：一个带 Mathlib 的 Lake 项目 - -Cowork 这边的沙盒没有 Lean，`check_statements.py` 和真正跑 `lean-agent`/ -`lean-bench` 都需要在你本机（或者别的有 Lean 的环境）完成。如果还没有这样一 -个项目： +### 7. Assemble proven library candidates into a reusable library file ```sh -cd ~/ProjectResearch # 随便一个地方 +python3 textbook/build_library.py library_candidates/goodman-1.6.jsonl \ + results/goodman-1.6-001-library/results.jsonl --out lib/Chapter01Section06.lean +``` + +(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. + +## How this is meant to connect to lean-agent + +This pipeline only produces data files; it is not the proof search itself. The +intended `lean-agent` workflow this feeds: + +1. Given a target statement, check whether it's even valid Lean (this is what + `check_statements.py` does ahead of time, so `lean-agent` doesn't waste attempts + on a statement that can't type-check no matter what). +2. Track the current proof state as a list of open goals (the same thing the + [vscode-lean4](https://github.com/leanprover/vscode-lean4) plugin shows you + live) -- not attempt the whole theorem in one LLM call. +3. At each step, search a database of already-proven statements (`lib/*.lean`, + built by `build_library.py`, plus Mathlib itself) for something applicable to + the current goal -- the equivalent of Lean's `exact?`/`apply?` tactics, or a + semantic/embedding search over the library -- and if something is used, apply it + and fold the resulting subgoals back into the open-goals list. +3. Repeat until the goal list is empty (theorem proved) or a budget is exhausted + (forced stop, left as an open goal / `sorry`). + +That proof-search loop isn't built yet -- `lean-bench`'s current `solve()` call is +still single-shot (one LLM call, checked by Lean, retried up to `--attempts` times +from scratch), not goal-directed. This pipeline's two-track split (bench targets +from exercises, growing library from proven body content) is what that loop will +need once it exists. + +## Local environment setup: a Lake project with Mathlib + +The Cowork sandbox has no Lean; `check_statements.py` and real `lean-agent`/ +`lean-bench` runs both need to happen on your machine (or anywhere else with Lean). +If you don't have such a project yet: + +```sh +cd ~/ProjectResearch # anywhere lake +leanprover/lean4:v4.33.1 new mathlib-bench math cd mathlib-bench -lake exe cache get # 下载 Mathlib 预编译缓存，比从源码编译快得多 -lake build +lake exe cache get # downloads Mathlib's precompiled cache -- much faster than building from source +lake build Mathlib # compiles Mathlib's own top-level .olean aggregator (cache get alone doesn't) ``` -之后 `--lean-project` 就指到 `mathlib-bench` 这个目录，`--lean-command` 用 -`'["lake","env","lean"]'`。 +Then point `--lean-project` at `mathlib-bench` and `--lean-command` at +`'["lake","env","lean"]'`. -## 反馈循环 +## Feedback loop -我（claude-bot）在 ProjectResearch 里生成/修改数据集和代码 → 提交并 push 到 -`Zayden-Jung/lean-bench`（用 claude-bot 的 token） → 你在本机 `git pull` → -跑 `check_statements.py` / `lean-bench` → 把失败的条目 id 和 Lean 报的错发 -给我 → 我改完再 push。不需要额外工具，就是正常的 git 往返。 +I (claude-bot) generate/edit files in ProjectResearch -> commit and push to +`Zayden-Jung/lean-bench` (using claude-bot's token) -> you `git pull` locally -> +run `check_statements.py` / `lean-bench` -> send back the failing ids and Lean's +diagnostics -> I fix and push again. Ordinary git round-trip, no extra tooling. diff --git a/textbook/build_definitions.py b/textbook/build_definitions.py new file mode 100644 index 0000000..ce3fdd5 --- /dev/null +++ b/textbook/build_definitions.py @@ -0,0 +1,55 @@ +"""Assemble a standalone, importable Lean 4 file from a definitions manifest's +hand-written lean_code entries. + +Only definitions with no Mathlib equivalent need one -- when a manifest entry's +mathlib_ref is set, the theorems that use it just reference that Mathlib name +directly, and there is nothing to assemble here. This exists because a definitions +manifest is only JSON metadata by itself: Lean can't verify a proof that mentions a +concept unless that concept is actual Lean code somewhere it can see, which is the +point raised about definitions needing to be real, not just documented. + +Does not call Lean itself -- check_statements.py / lean-agent still has to actually +verify that the resulting file, and anything that imports it, type-checks. +""" +import argparse +import json +from pathlib import Path + + +def build(definitions_paths): + entries = [] + for path in definitions_paths: + entries.extend(json.loads(path.read_text(encoding='utf-8'))) + + lines = ['-- Generated by textbook/build_definitions.py -- hand-written Lean', + '-- definitions for concepts with no Mathlib equivalent. Regenerate', + '-- from the definitions manifest(s) instead of hand-editing.', + '', 'import Mathlib', ''] + emitted = 0 + for entry in entries: + code = entry.get('lean_code') + if not code: + continue + lines.append(f"-- {entry['label']}: {entry['concept']}") + if entry.get('notes'): + for note_line in entry['notes'].splitlines(): + lines.append(f"-- {note_line}") + lines.append(code.rstrip()) + lines.append('') + emitted += 1 + return '\n'.join(lines), emitted + + +def main(): + parser = argparse.ArgumentParser(description='Assemble hand-written definitions into one importable Lean file') + parser.add_argument('definitions', type=Path, nargs='+', help='one or more *.definitions.json manifests') + parser.add_argument('--out', type=Path, required=True) + args = parser.parse_args() + + text, emitted = build(args.definitions) + args.out.write_text(text + '\n', encoding='utf-8') + print(f'{emitted} hand-written definitions -> {args.out}') + + +if __name__ == '__main__': + main() diff --git a/textbook/exercises_1_6.index.json b/textbook/exercises_1_6.index.json new file mode 100644 index 0000000..08df20a --- /dev/null +++ b/textbook/exercises_1_6.index.json @@ -0,0 +1,62 @@ +[ + { + "number": "1.6.1", + "first_line": "1.6.1. Complete the following sketch of a proof of Proposition 1.6.7 using" + }, + { + "number": "1.6.2", + "first_line": "1.6.2. Prove Proposition 1.6.9. Hint: For part (b), you have to show that" + }, + { + "number": "1.6.3", + "first_line": "1.6.3. Suppose that a natural number p > 1 has the property that for all" + }, + { + "number": "1.6.4", + "first_line": "1.6.4. For each of the following pairs of numbers m; n, compute" + }, + { + "number": "1.6.5", + "first_line": "1.6.5. Show that for nonzero integers m and n, g:c:d:.m; n/ D" + }, + { + "number": "1.6.6", + "first_line": "1.6.6. Show that for nonzero integers m and n, g:c:d:.m; n/ is the largest" + }, + { + "number": "1.6.7", + "first_line": "1.6.7. Show that if p is a prime number and a is any nonzero integer, then" + }, + { + "number": "1.6.8", + "first_line": "1.6.8. Suppose that a and b are relatively prime integers and that x is an" + }, + { + "number": "1.6.9", + "first_line": "1.6.9. Show that if a prime number p divides a product a1 a2 : : : ar of" + }, + { + "number": "1.6.10", + "first_line": "1.6.10." + }, + { + "number": "1.6.11", + "first_line": "1.6.11. Let n1 ; : : : ; nk be nonzero integers. Let d D g:c:d.n1 ; : : : ; nk /," + }, + { + "number": "1.6.12", + "first_line": "1.6.12. Let n1 ; : : : ; nk be nonzero integers." + }, + { + "number": "1.6.13", + "first_line": "1.6.13." + }, + { + "number": "1.6.14", + "first_line": "1.6.14. Show two nonzero integers are relatively prime if and only if they" + }, + { + "number": "1.6.15", + "first_line": "1.6.15. Prove Lemma 1.6.26. You may use the uniqueness of the prime" + } +] diff --git a/textbook/extract_exercises.py b/textbook/extract_exercises.py new file mode 100644 index 0000000..8cf965c --- /dev/null +++ b/textbook/extract_exercises.py @@ -0,0 +1,101 @@ +"""Slice the 'Exercises N.N' block out of a pdftotext -layout dump and list its +numbered problems, as input for formalize_exercises.py. + +Mirrors extract_section.py but for the exercise list at the end of a section, which +uses bare 'N.N.N.' numbering at the start of a line (no Theorem/Proposition keyword) +instead of labeled Theorem/Proposition/Lemma/Corollary/Definition entries. Exercise +numbers are their own independent sequence (Exercise 1.6.5 has nothing to do with +Proposition/Theorem/Lemma/Corollary/Definition 1.6.5 in the body) -- keep their ids +namespaced separately downstream so the two never collide. + +A known false-positive source: a sentence like "...converse of Proposition\n1.6.19." +can wrap so the bare number lands alone at the start of a line, which looks +identical to a real exercise heading. numbered_items() drops any item whose number +jumps ahead of the running sequence by more than --max-gap AND has no text on its +own line (a real item almost always has problem text right after the number; a +wrapped cross-reference is just the number and a period). Dropped candidates are +still reported, never silently discarded. +""" +import argparse +import json +import re +import sys +from pathlib import Path + +ITEM_RE = re.compile(r'^(\d+\.\d+\.\d+)\.\s*(.*)$') + + +def find_heading_line(lines, heading): + for i, line in enumerate(lines): + if line.strip() == heading: + return i + raise ValueError(f'Heading not found: {heading!r}') + + +def extract_exercises(full_text, start_heading, end_heading): + lines = full_text.split('\n') + start = find_heading_line(lines, start_heading) + end = find_heading_line(lines, end_heading) if end_heading else len(lines) + if end <= start: + raise ValueError('end_heading must come after start_heading') + return '\n'.join(lines[start:end]) + + +def numbered_items(exercises_text, section_prefix, max_gap=3): + """Unique numbered items in exercises_text whose number starts with + section_prefix (e.g. '1.6.'), keeping only the first occurrence of each number + (a running page header can repeat text near a page break). Returned in book + order (numeric, not lexical). See module docstring for the wrapped-cross- + reference false-positive filter; dropped candidates are returned separately so + callers can report them instead of silently losing items.""" + seen = {} + for line in exercises_text.split('\n'): + line = line.strip() + m = ITEM_RE.match(line) + if not m: + continue + number, rest = m.group(1), m.group(2) + if not number.startswith(section_prefix) or number in seen: + continue + seen[number] = {"number": number, "first_line": line[:120], "rest_empty": not rest.strip()} + + def sort_key(item): + return tuple(int(p) for p in item['number'].split('.')) + + ordered = sorted(seen.values(), key=sort_key) + kept, dropped = [], [] + last_n = 0 + for item in ordered: + n = int(item['number'].split('.')[-1]) + if item['rest_empty'] and last_n and (n - last_n) > max_gap: + dropped.append(item) + continue + kept.append({"number": item['number'], "first_line": item['first_line']}) + last_n = n + return kept, dropped + + +def main(): + parser = argparse.ArgumentParser(description='Slice one "Exercises N.N" block out of a pdftotext -layout dump') + parser.add_argument('layout_txt', type=Path) + parser.add_argument('--start-heading', required=True, help="e.g. 'Exercises 1.6'") + parser.add_argument('--end-heading', help="e.g. '1.7. Modular Arithmetic'; omit for end of file") + parser.add_argument('--section-prefix', required=True, help="e.g. '1.6.'") + parser.add_argument('--max-gap', type=int, default=3, help='see module docstring') + parser.add_argument('--out-text', type=Path, required=True) + parser.add_argument('--out-index', type=Path, required=True) + args = parser.parse_args() + + full_text = args.layout_txt.read_text(encoding='utf-8') + exercises_text = extract_exercises(full_text, args.start_heading, args.end_heading) + args.out_text.write_text(exercises_text, encoding='utf-8') + index, dropped = numbered_items(exercises_text, args.section_prefix, args.max_gap) + args.out_index.write_text(json.dumps(index, ensure_ascii=False, indent=2) + '\n', encoding='utf-8') + print(f'{len(index)} numbered exercises -> {args.out_index}') + for item in dropped: + print(f" dropped as likely a wrapped cross-reference, not a real exercise: {item['number']}" + f" ({item['first_line']!r})", file=sys.stderr) + + +if __name__ == '__main__': + main() diff --git a/textbook/formalize_exercises.py b/textbook/formalize_exercises.py new file mode 100644 index 0000000..cd5a5b8 --- /dev/null +++ b/textbook/formalize_exercises.py @@ -0,0 +1,185 @@ +"""LLM-assisted formalization of a section's EXERCISES into Lean 4 bench targets. + +These are the real lean-bench targets: problems the reader is meant to solve, as +opposed to formalize.py, which turns the book's own stated Theorems/Propositions/ +Lemmas/Corollaries into a *candidate library* -- premises meant to be proven once +and then reused, not exam questions. See textbook/README.md for the split. + +Exercises often reference the body by number instead of restating the claim (e.g. +"1.6.2. Prove Proposition 1.6.9.", or "1.6.15. Prove Lemma 1.6.26."), so this script +gives the model the exercise text *and* the full body section text together, and +tells it to resolve such references into a self-contained statement using the +body's actual content -- never leave a Lean statement that just says "the thing +Exercise N asks for" without spelling out what that thing is. + +Same caveats as formalize.py: never runs Lean itself, the source PDF's math symbols +can be corrupted, and output must go through check_statements.py before trusting it +or spending lean-agent proof attempts on it. +""" +import argparse +import json +import re +from pathlib import Path + +try: + from .llm import ChatClient, load_dotenv + from .formalize import extract_json_block +except ImportError: + from llm import ChatClient, load_dotenv + from formalize import extract_json_block + +SYSTEM_PROMPT = """You are formalizing the EXERCISES of one section of an \ +undergraduate abstract algebra textbook (Goodman, "Algebra: Abstract and \ +Concrete") into Lean 4 bench targets using Mathlib. + +You will receive: +1. The book's own Theorem/Proposition/Lemma/Corollary/Definition statements for \ +this section (body text), for reference. +2. The section's numbered exercises (their own independent numbering, unrelated to \ +the body's numbering -- Exercise 1.6.5 has nothing to do with body item 1.6.5). +3. A checklist of every exercise number in this section, so you know exactly what \ +to cover. EVERY number in the checklist MUST appear in your output as at least one \ +entry (an excluded one is fine, e.g. for a pure computation -- see below -- but \ +silently leaving a checklist number out entirely is never acceptable and your \ +output will be rejected if you do this). Do not invent numbers that are not listed. + +WARNING: the source PDF's math font encoding is broken in this extraction -- \ +symbols like congruence, set membership, comparisons, superscripts and subscripts \ +are frequently dropped or garbled. Use your own knowledge of standard undergraduate \ +number theory / algebra to reconstruct the intended mathematics from context; do \ +not invent content that is not actually in the section. + +Many exercises say things like "Prove Proposition 1.6.9" or "Prove Lemma 1.6.26" \ +instead of restating a claim. For those, use the body text to find what that \ +referenced item actually says, and write ITS full claim as the Lean statement -- \ +never emit something like "the statement of Proposition 1.6.9" as a placeholder; \ +the reader of your output has no access to the body text, only the Lean statement. + +An exercise with lettered sub-parts (a), (b), (c) that each state an independent \ +provable claim should become one entry PER PART (id suffixed "-a", "-b", ... in \ +part order), the same way the body pipeline splits multi-part propositions. Keep a \ +single entry for one exercise if its parts are really one claim you naturally \ +express as a single Lean statement (e.g. an iff with two directions written as \ +separate parts). + +Produce exactly one JSON object with a single key "exercises" (a JSON array), \ +inside one ```json fenced code block, and nothing else outside that block. + +Each element of "exercises": +{ + "id": "goodman-1-6-ex-5", + "source_label": "Exercise 1.6.5", + "kind": "exercise", + "statement": "the Lean 4 proposition only, i.e. what goes after `theorem name : `, \ +using Mathlib vocabulary wherever possible instead of reinventing definitions", + "prelude": "Lean import lines (and, rarely, a small needed `def`) this statement \ +needs, usually just \\"import Mathlib\\"", + "natural_language": "a short original English restatement in your own words (do \ +not quote the source text verbatim)", + "requires": ["list of Mathlib identifiers the statement uses"], + "references": ["body labels this exercise restates or depends on, e.g. \ +'Proposition 1.6.9', or [] if none"], + "include_in_bench": true, + "exclude_reason": null +} + +Set "include_in_bench" to false (with a short "exclude_reason") instead of omitting \ +an entry when an exercise is not a genuine general claim to formalize and prove -- \ +e.g. it asks the reader to write a computer program, perform one specific numeric \ +computation with no general statement, answer a yes/no or "discuss" question with \ +no single formal claim, or the extracted text is too corrupted to recover its \ +meaning confidently -- still emit the entry so nothing silently disappears, just \ +mark it excluded. + +id must be "goodman-" + section-prefix-with-hyphens + "-ex-" + the exercise's own \ +last number component (and a lettered suffix for sub-parts), e.g. Exercise 1.6.5 -> \ +"goodman-1-6-ex-5", part (a) of Exercise 1.6.11 -> "goodman-1-6-ex-11-a". Do not \ +include a proof, "sorry", or "by" -- statement is only the proposition, no theorem \ +keyword or name. Do not wrap the JSON in anything other than a single ```json \ +fenced block.""" + + +def user_prompt(section_text, exercises_text, checklist): + checklist_lines = '\n'.join(f"- Exercise {item['number']}: {item['first_line']}" + for item in checklist) + return (f"Checklist of exercise numbers in this section:\n{checklist_lines}\n\n" + f"Body text (for resolving 'Prove Proposition N.N.N'-style references):\n" + f"{section_text}\n\n" + f"Exercises text:\n{exercises_text}") + + +def validate(data, checklist=None): + if not isinstance(data, dict) or 'exercises' not in data: + raise ValueError('Response must be a JSON object with an "exercises" array') + exercises = data['exercises'] + if not isinstance(exercises, list): + raise ValueError('"exercises" must be an array') + seen_ids = set() + covered_numbers = set() + for item in exercises: + for field in ('id', 'source_label', 'statement', 'prelude', 'include_in_bench'): + if field not in item: + raise ValueError(f'exercise entry missing field {field!r}: {item}') + if item['id'] in seen_ids: + raise ValueError(f'Duplicate exercise id: {item["id"]}') + seen_ids.add(item['id']) + # "Exercise 1.6.11(a)" or "Exercise 1.6.11" -> "1.6.11" + m = re.search(r'(\d+\.\d+\.\d+)', item['source_label']) + if m: + covered_numbers.add(m.group(1)) + if checklist is not None: + expected = {c['number'] for c in checklist} + missing = expected - covered_numbers + if missing: + raise ValueError( + 'Model silently dropped checklist items instead of marking them ' + 'include_in_bench=false with a reason (never allowed): ' + + ', '.join(sorted(missing, key=lambda s: tuple(int(p) for p in s.split('.')))) + ) + return exercises + + +def main(): + parser = argparse.ArgumentParser(description='LLM-formalize a section\'s exercises into Lean 4 bench targets') + parser.add_argument('section_text', type=Path, help='body text, from extract_section.py') + parser.add_argument('exercises_text', type=Path, help='from extract_exercises.py') + parser.add_argument('exercises_index', type=Path, help='from extract_exercises.py') + parser.add_argument('--out-dataset', type=Path, required=True, help='JSONL of exercises with include_in_bench=true') + parser.add_argument('--out-excluded', type=Path, help='JSONL of exercise entries the model excluded, for review') + parser.add_argument('--model', required=True) + parser.add_argument('--base-url', default='https://dashscope.aliyuncs.com/compatible-mode/v1') + parser.add_argument('--api-key-env', default='DASHSCOPE_API_KEY') + parser.add_argument('--env-file', type=Path, default=Path(__file__).resolve().parents[1] / '.env') + parser.add_argument('--timeout', type=float, default=300) + args = parser.parse_args() + + load_dotenv(args.env_file) + client = ChatClient(args.model, args.base_url, args.api_key_env, args.timeout) + checklist = json.loads(args.exercises_index.read_text(encoding='utf-8')) + section_text = args.section_text.read_text(encoding='utf-8') + exercises_text = args.exercises_text.read_text(encoding='utf-8') + messages = [{"role": "system", "content": SYSTEM_PROMPT}, + {"role": "user", "content": user_prompt(section_text, exercises_text, checklist)}] + reply = client.complete(messages) + data = extract_json_block(reply) + exercises = validate(data, checklist) + + included = [t for t in exercises if t.get('include_in_bench')] + excluded = [t for t in exercises if not t.get('include_in_bench')] + + with args.out_dataset.open('w', encoding='utf-8') as stream: + for item in included: + stream.write(json.dumps(item, ensure_ascii=False) + '\n') + if args.out_excluded: + with args.out_excluded.open('w', encoding='utf-8') as stream: + for item in excluded: + stream.write(json.dumps(item, ensure_ascii=False) + '\n') + + print(f'{len(included)} exercises -> {args.out_dataset}') + if excluded: + note = f' (see {args.out_excluded})' if args.out_excluded else ' (pass --out-excluded to keep them)' + print(f'{len(excluded)} excluded{note}') + + +if __name__ == '__main__': + main() diff --git a/textbook/goodman-1.6-exercises.excluded.jsonl b/textbook/goodman-1.6-exercises.excluded.jsonl new file mode 100644 index 0000000..bb6d8e9 --- /dev/null +++ b/textbook/goodman-1.6-exercises.excluded.jsonl @@ -0,0 +1,4 @@ +{"id": "goodman-1-6-ex-4", "source_label": "Exercise 1.6.4", "kind": "exercise", "statement": "gcd 60 8 = 4 ∧ 4 = 60 * a + 8 * b ∧ gcd 32242 42 = 2 ∧ 2 = 32242 * c + 42 * d", "prelude": "import Mathlib.Data.Int.GCD", "natural_language": "Compute the greatest common divisor of (a) 60 and 8, and (b) 32242 and 42, and express each as an integer linear combination of the given numbers.", "requires": ["Mathlib.Data.Int.GCD"], "references": [], "include_in_bench": false, "exclude_reason": "Specific numeric computation"} +{"id": "goodman-1-6-ex-10", "source_label": "Exercise 1.6.10", "kind": "exercise", "statement": "Write a program in your favorite programming language to compute the greatest common divisor of two nonzero integers, using the approach of repeated division with remainders. Get your program to explicitly give the greatest common divisor as an integer linear combination of the given nonzero integers. Compare this method with the method of computing the prime factorizations of the two integers and taking the largest collection of prime factors common to the two factorizations in terms of computational efficiency.", "prelude": "", "natural_language": "Write a program to compute the GCD of two integers and compare it with the prime factorization method.", "requires": [], "references": [], "include_in_bench": false, "exclude_reason": "Programming task and discussion question"} +{"id": "goodman-1-6-ex-13", "source_label": "Exercise 1.6.13", "kind": "exercise", "statement": "(a) Develop an algorithm to compute gcd(n₁, n₂, ..., nₖ). (b) Develop a computer program to compute the greatest common divisor of any finite collection of nonzero integers.", "prelude": "", "natural_language": "(a) Develop an algorithm to compute the GCD of n₁, n₂, ..., nₖ. (b) Develop a computer program to compute the GCD of any finite collection of nonzero integers.", "requires": [], "references": [], "include_in_bench": false, "exclude_reason": "Algorithm and programming task"} +{"id": "goodman-1-6-ex-12-a", "source_label": "Exercise 1.6.12(a)", "kind": "exercise", "statement": "N/A", "prelude": "import Mathlib", "natural_language": "Whether relatively prime implies pairwise relatively prime for more than two integers.", "requires": [], "references": [], "include_in_bench": false, "exclude_reason": "Discussion/judgment question, not a fixed claim; and taken as an unconditional identity it is false in general (e.g. 6, 10, 15 are jointly coprime but not pairwise coprime)."} diff --git a/textbook/goodman-1.6.definitions.json b/textbook/goodman-1.6.definitions.json index e5b18f2..523a7c2 100644 --- a/textbook/goodman-1.6.definitions.json +++ b/textbook/goodman-1.6.definitions.json @@ -24,8 +24,8 @@ "label": "Definition 1.6.22", "concept": "greatest common divisor (gcd) of several integers", "mathlib_ref": null, - "lean_code": null, - "notes": "Corrected from an earlier hallucinated `GCD.gcd` (no such constant exists). Mathlib has no single ready-made 'gcd of a `List ℤ`' constant matching the book's definition verbatim; the pipeline instead states the gcd's defining property directly as an explicit existential (d divides every element, and every common divisor divides d) in the corresponding bench statement (goodman-1-6-24) rather than invoking a nonexistent name." + "lean_code": "def IsGCDOfList (d : ℕ) (as : List ℤ) : Prop :=\n (∀ a ∈ as, (d:ℤ) ∣ a) ∧ ∀ e : ℤ, (∀ a ∈ as, e ∣ a) → e ∣ (d:ℤ)", + "notes": "No single ready-made Mathlib constant for 'gcd of a `List ℤ`' matches the book's definition verbatim, so this concept gets a real, hand-written Lean `def` (see lean_code) instead of only a JSON pointer -- it is compiled into textbook/lib/Definitions.lean by build_definitions.py and inlined into any statement's `prelude` that needs it, so Lean can actually elaborate proofs that use it, not just read a description of it." }, { "label": "Definition 1.6.25",