From 79c728567a185ae7c1e34cb9af6cd77225675589 Mon Sep 17 00:00:00 2001 From: Claude Bot Date: Fri, 18 Sep 2026 16:50:34 +0000 Subject: [PATCH] Fix 10 failing goodman-1.6 statements based on Lean compiler diagnostics All 21 statements in datasets/goodman-1.6.jsonl now elaborate cleanly (verified locally via check_statements.py, 11/21 passing before this change). Fixes applied, one per failing id: - goodman-1-6-7: single-binder existential-unique over a pair (qr : ZxZ) instead of the invalid two-binder 'exists unique' form. - goodman-1-6-10: rewrote set-builder notation to the explicit {v | exists a b, v = ...} form. - goodman-1-6-11: replaced 'let d := ... in ...' with the required semicolon form 'let d := ...; ...', and added the missing Nat-to-Int casts on d. - goodman-1-6-17: added explicit Nat-to-Int coercions on the three divisibility relations. - goodman-1-6-18: changed p from Z to N (Nat.Prime requires N), added casts, and replaced the nonexistent Int.Coprime with IsCoprime. - goodman-1-6-19: changed p from Z to N and added the matching casts. - goodman-1-6-20: changed p from Z to N, added casts, and fixed the quantifier structure so the prime-divides-product hypothesis is not nested inside the per-element forall. - goodman-1-6-23: replaced the Fin n literal comparison 'j = 0' (which needs a NeZero instance) with 'j.val = 0'. - goodman-1-6-24: replaced the invalid bare '(*)' operator section with '(fun x y => x * y)'-equivalent '(. * .)', and replaced the nonexistent GCD.gcd with an explicit existential statement of the gcd property (divides every element; every common divisor divides it). - goodman-1-6-26: replaced the nonexistent Int.Coprime with IsCoprime. Also corrected the three parallel hallucinated Mathlib refs in textbook/goodman-1.6.definitions.json (Int.Coprime, GCD.gcd, Int.PairwiseCoprime -> IsCoprime, null with notes, and List.Pairwise IsCoprime respectively), since the Lean compiler confirms none of the original names exist. Co-Authored-By: Claude Sonnet 5 Claude-Session: https://claude.ai/code/session_017vbLFFJiHSZqGZHEkjvG5x --- datasets/goodman-1.6.jsonl | 20 ++++++++++---------- textbook/goodman-1.6.definitions.json | 12 ++++++------ 2 files changed, 16 insertions(+), 16 deletions(-) diff --git a/datasets/goodman-1.6.jsonl b/datasets/goodman-1.6.jsonl index ca5a970..1270a81 100644 --- a/datasets/goodman-1.6.jsonl +++ b/datasets/goodman-1.6.jsonl @@ -1,20 +1,20 @@ {"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 → ∃! (q r : ℤ), a = q * d + r ∧ 0 ≤ r < 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-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 ∈ {a * m + b * n | a b : ℤ} → ∀ (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) in d = Int.gcd m n ∧ d ∈ {a * m + b * n | a b : ℤ}", "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-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 ∨ Int.Coprime 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-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 = 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 ℤ), d = GCD.gcd as ∧ 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-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 → Int.Coprime (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-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-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} diff --git a/textbook/goodman-1.6.definitions.json b/textbook/goodman-1.6.definitions.json index 1099537..e5b18f2 100644 --- a/textbook/goodman-1.6.definitions.json +++ b/textbook/goodman-1.6.definitions.json @@ -16,22 +16,22 @@ { "label": "Definition 1.6.14", "concept": "relatively prime integers", - "mathlib_ref": "Int.Coprime", + "mathlib_ref": "IsCoprime", "lean_code": null, - "notes": "The definition in the book is consistent with Mathlib's definition of coprime integers." + "notes": "Corrected from an earlier hallucinated `Int.Coprime` (no such constant exists). Mathlib's `IsCoprime a b` (in a commutative semiring, so usable for ℤ) captures relative primality via Bezout-style coefficients and is definitionally the right notion here." }, { "label": "Definition 1.6.22", "concept": "greatest common divisor (gcd) of several integers", - "mathlib_ref": "GCD.gcd", + "mathlib_ref": null, "lean_code": null, - "notes": "The definition in the book is consistent with Mathlib's generalization of gcd to multiple integers." + "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." }, { "label": "Definition 1.6.25", "concept": "pairwise relatively prime integers", - "mathlib_ref": "Int.PairwiseCoprime", + "mathlib_ref": "List.Pairwise IsCoprime", "lean_code": null, - "notes": "The definition in the book is consistent with Mathlib's definition of pairwise coprime integers." + "notes": "Corrected from an earlier hallucinated `Int.PairwiseCoprime` (no such constant exists). Pairwise relative primality of a list is expressed as `List.Pairwise IsCoprime as` (or `List.Pairwise (IsCoprime ·) as`), combining the general `List.Pairwise` relation with `IsCoprime`, rather than via a single dedicated name." } ]