diff --git a/database/goodman-1.6.index.jsonl b/database/goodman-1.6.index.jsonl index 6d08804..f1911cb 100644 --- a/database/goodman-1.6.index.jsonl +++ b/database/goodman-1.6.index.jsonl @@ -1,21 +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"]} +{"name": "goodman_1_6_1", "id": "goodman-1-6-1", "source_label": "Proposition 1.6.1", "kind": "proposition", "status": "proof_pending", "proof": "intro a b c\nrefine ⟨by ring, by ring, by ring, by ring, by ring, by ring, by ring, by ring, ?_⟩\nintro x y h\nexact ⟨fun hx => h (by simp [hx]), fun hy => h (by simp [hy])⟩", "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": "proof_pending", "proof": "intro n hn\nobtain ⟨p, hp, hpd⟩ := Nat.exists_prime_and_dvd (show n ≠ 1 by omega)\nexact ⟨p, hp, hpd⟩", "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", "proof": null, "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", "proof": null, "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", "proof": null, "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", "proof": null, "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", "proof": null, "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", "proof": null, "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": "proof_pending", "proof": "intro m n _\nrw [Int.gcd_eq_one_iff_coprime]\nconstructor\n· intro h\n obtain ⟨u, v, huv⟩ := h\n exact ⟨u, v, huv⟩\n· intro h\n obtain ⟨s, t, hst⟩ := h\n exact ⟨s, t, hst⟩", "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": "proof_pending", "proof": "intro a b x h\nexact IsCoprime.mul_dvd (Nat.isCoprime_iff_coprime.mpr h.1) h.2.1 h.2.2", "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", "proof": null, "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": "proof_pending", "proof": "intro p a b h hdvd\nexact Int.Prime.dvd_mul' h.1 hdvd", "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": "proof_pending", "proof": "intro p as hp _ h\nobtain ⟨a, ha, hpa⟩ := (Nat.Prime.prime_int hp).dvd_prod_iff.mp h\nexact ⟨a, ha, hpa⟩", "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", "proof": null, "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", "proof": null, "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", "proof": null, "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", "proof": null, "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": "proof_pending", "proof": "intro u v h\nexact Int.mul_eq_one_iff_eq_one_or_neg_one.mp h", "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": "proof_pending", "proof": "intro a b h\nexact Int.associated_iff.mp (associated_of_dvd_dvd h.1 h.2)", "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": "proof_pending", "proof": "intro a b c h\nexact dvd_trans h.1 h.2", "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": "proof_pending", "proof": "intro a b c s t h\nexact dvd_add (h.1.mul_left s) (h.2.mul_left t)", "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/database/goodman-1.6.jsonl b/database/goodman-1.6.jsonl index 318777c..7a33cf0 100644 --- a/database/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, "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-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, "proof": "intro a b c\nrefine ⟨by ring, by ring, by ring, by ring, by ring, by ring, by ring, by ring, ?_⟩\nintro x y h\nexact ⟨fun hx => h (by simp [hx]), fun hy => h (by simp [hy])⟩", "proof_checked": false} +{"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, "proof": "intro n hn\nobtain ⟨p, hp, hpd⟩ := Nat.exists_prime_and_dvd (show n ≠ 1 by omega)\nexact ⟨p, hp, hpd⟩", "proof_checked": false} {"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-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, "proof": "intro m n _\nrw [Int.gcd_eq_one_iff_coprime]\nconstructor\n· intro h\n obtain ⟨u, v, huv⟩ := h\n exact ⟨u, v, huv⟩\n· intro h\n obtain ⟨s, t, hst⟩ := h\n exact ⟨s, t, hst⟩", "proof_checked": false} +{"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, "proof": "intro a b x h\nexact IsCoprime.mul_dvd (Nat.isCoprime_iff_coprime.mpr h.1) h.2.1 h.2.2", "proof_checked": false} {"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-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, "proof": "intro p a b h hdvd\nexact Int.Prime.dvd_mul' h.1 hdvd", "proof_checked": false} +{"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, "proof": "intro p as hp _ h\nobtain ⟨a, ha, hpa⟩ := (Nat.Prime.prime_int hp).dvd_prod_iff.mp h\nexact ⟨a, ha, hpa⟩", "proof_checked": false} {"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} +{"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, "proof": "intro u v h\nexact Int.mul_eq_one_iff_eq_one_or_neg_one.mp h", "proof_checked": false} +{"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, "proof": "intro a b h\nexact Int.associated_iff.mp (associated_of_dvd_dvd h.1 h.2)", "proof_checked": false} +{"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, "proof": "intro a b c h\nexact dvd_trans h.1 h.2", "proof_checked": false} +{"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, "proof": "intro a b c s t h\nexact dvd_add (h.1.mul_left s) (h.2.mul_left t)", "proof_checked": false} diff --git a/lib/Goodman/Chapter01Section06.lean b/lib/Goodman/Chapter01Section06.lean index 1ccc07d..75dbf69 100644 --- a/lib/Goodman/Chapter01Section06.lean +++ b/lib/Goodman/Chapter01Section06.lean @@ -8,10 +8,10 @@ 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. -/ +/-- 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; a proof is recorded but not yet verified. -/ 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. -/ +/-- 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; a proof is recorded but not yet verified. -/ 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. -/ @@ -32,19 +32,19 @@ axiom goodman_1_6_11 : ∀ (m n : ℤ), m ≠ 0 ∧ n ≠ 0 → let d := Nat.gcd /-- 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. -/ +/-- 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; a proof is recorded but not yet verified. -/ 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. -/ +/-- 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; a proof is recorded but not yet verified. -/ 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. -/ +/-- 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; a proof is recorded but not yet verified. -/ 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. -/ +/-- 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; a proof is recorded but not yet verified. -/ 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. -/ @@ -59,15 +59,15 @@ axiom goodman_1_6_24 : ∀ (as : List ℤ), as.length ≥ 2 → (∀ (a : ℤ), /-- 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. -/ +/-- 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; a proof is recorded but not yet verified. -/ 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. -/ +/-- 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; a proof is recorded but not yet verified. -/ 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. -/ +/-- Proposition 1.6.2 (Goodman, Algebra: Abstract and Concrete). Divisibility of integers is transitive. ASSERTED from the textbook; a proof is recorded but not yet verified. -/ 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. -/ +/-- 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; a proof is recorded but not yet verified. -/ 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 index 3f8b4c3..bcb53f3 100644 --- a/tests/test_build_database.py +++ b/tests/test_build_database.py @@ -57,6 +57,22 @@ class BuildDatabaseTests(unittest.TestCase): self.assertEqual(skipped, ['goodman-1-6-24']) self.assertEqual(len(index), 1) + def test_recorded_proof_counts_only_once_checked(self): + # An unverified proof must NOT be emitted as a theorem -- the library may + # never claim more than Lean has confirmed. + pending = [dict(ENTRIES[0], proof='ring', proof_checked=False)] + text, index, _e, _s = build(pending) + self.assertIn('axiom goodman_1_6_1 :', text) + self.assertNotIn('theorem goodman_1_6_1 :', text) + self.assertEqual(index[0]['status'], 'proof_pending') + self.assertEqual(index[0]['proof'], 'ring') + + checked = [dict(ENTRIES[0], proof='ring', proof_checked=True)] + text, index, _e, _s = build(checked) + self.assertIn('theorem goodman_1_6_1 :', text) + self.assertIn(' ring', text) + self.assertEqual(index[0]['status'], 'proved') + def test_index_carries_identifiers_and_strips_fix_notes(self): _text, index, _emitted, _skipped = build(ENTRIES) first = index[0] diff --git a/tests/test_check_proofs.py b/tests/test_check_proofs.py new file mode 100644 index 0000000..62d56ee --- /dev/null +++ b/tests/test_check_proofs.py @@ -0,0 +1,40 @@ +import unittest + +from textbook.check_proofs import ALLOWED_AXIOMS, AXIOM_LINE, check_proof + + +class CheckProofsTests(unittest.TestCase): + """Only the Lean-free logic is unit-tested here; actually compiling a proof needs + Lean and Mathlib, which is what running check_proofs.py on a real machine does.""" + + def test_missing_proof_fails_without_invoking_lean(self): + result = check_proof('t', 'True', '') + self.assertFalse(result.ok) + self.assertIn('no proof recorded', result.diagnostics) + + def test_sorry_is_rejected_without_invoking_lean(self): + for escape in ('sorry', 'admit', 'native_decide'): + result = check_proof('t', 'True', f'intro h\n{escape}') + self.assertFalse(result.ok, escape) + self.assertIn(escape, result.diagnostics) + + def test_proof_mentioning_sorry_only_as_substring_is_not_rejected_for_that(self): + # 'sorryAx' contains 'sorry' but \b...\b must not match a longer identifier, + # otherwise a legitimate name would be banned by accident. + from textbook.check_proofs import BANNED + self.assertIsNone(BANNED.search('exact notsorryreally')) + self.assertIsNotNone(BANNED.search('exact sorry')) + + def test_axiom_line_parsing_separates_standard_from_ours(self): + line = "'goodman_1_6_1' depends on axioms: [propext, Classical.choice, Quot.sound]" + used = {a.strip() for a in AXIOM_LINE.search(line).group(1).split(',')} + self.assertEqual(used - ALLOWED_AXIOMS, set()) + + def test_axiom_line_parsing_flags_a_book_asserted_axiom(self): + line = "'x' depends on axioms: [propext, goodman_1_6_7, sorryAx]" + used = {a.strip() for a in AXIOM_LINE.search(line).group(1).split(',')} + self.assertEqual(used - ALLOWED_AXIOMS, {'goodman_1_6_7', 'sorryAx'}) + + +if __name__ == '__main__': + unittest.main() diff --git a/textbook/README.md b/textbook/README.md index 65bbb73..9eddbf6 100644 --- a/textbook/README.md +++ b/textbook/README.md @@ -169,7 +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. Generate the citable premise database +### 7. Verify recorded proofs + +A database entry may carry a `proof` (hand-written, or authored by an agent outside +a bench run), but it stays an `axiom` until Lean compiles it -- an unverified proof +never upgrades an entry, so the library cannot claim more than Lean confirmed. + +```sh +python3 textbook/check_proofs.py database/goodman-1.6.jsonl \ + --lean-project /path/to/your/mathlib-project \ + --lean-command '["lake","env","lean"]' \ + --report textbook/goodman-1.6.proof-report.jsonl \ + --update +``` + +Stricter than check_statements.py: it compiles `theorem ... := by `, rejects +`sorry`/`admit`/`native_decide`, and reads `#print axioms` to reject a proof that +depends on anything beyond Lean's own three axioms -- notably one that leans on a +book-asserted `axiom` from this very database, which would not be an independent +proof. `--update` writes `proof_checked` back, which is what promotes an entry on +the next build. + +### 8. Generate the citable premise database ```sh python3 textbook/build_database.py database/goodman-1.6.jsonl \ diff --git a/textbook/build_database.py b/textbook/build_database.py index 0ced177..794becc 100644 --- a/textbook/build_database.py +++ b/textbook/build_database.py @@ -98,20 +98,33 @@ def build(entries, results=None, require_checked=False): name = decl_name(entry_id) result = results.get(entry_id) - proved = bool(result and result.get('success') and result.get('attempts')) + # A proof can come from a lean-bench run, or be recorded on the entry itself + # (hand-written, or authored by an agent outside a bench run). Either way it + # only counts once check_proofs.py has actually compiled it: an unverified + # proof stays an axiom, so the library never claims more than Lean confirmed. + run_proof = result['attempts'][-1]['proof'] if ( + result and result.get('success') and result.get('attempts')) else None + own_proof = entry.get('proof') if entry.get('proof_checked') else None + proof = run_proof or own_proof + proved = bool(proof) + proof_pending = bool(not proved and entry.get('proof')) 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.') + ' -/' + if proved: + doc += ' Proof verified by Lean.' + elif proof_pending: + doc += ' ASSERTED from the textbook; a proof is recorded but not yet verified.' + else: + doc += ' ASSERTED from the textbook, not proven here.' + doc += ' -/' 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()) + lines.extend(' ' + line for line in proof.strip().splitlines()) else: lines.append(f'axiom {name} : {entry["statement"]}') lines.append('') @@ -121,7 +134,8 @@ def build(entries, results=None, require_checked=False): "id": entry_id, "source_label": entry.get('source_label'), "kind": entry.get('kind'), - "status": "proved" if proved else "asserted", + "status": "proved" if proved else ("proof_pending" if proof_pending else "asserted"), + "proof": proof if proved else entry.get('proof'), "statement": entry['statement'], "natural_language": entry.get('natural_language', '').split('[fix note:')[0].strip(), "identifiers": statement_identifiers(entry['statement']), @@ -154,7 +168,9 @@ def main(): 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)') + pending = sum(1 for r in index if r['status'] == 'proof_pending') + print(f'{len(emitted)} premises -> {args.out_lean} ({proved} proven, ' + f'{len(emitted) - proved} asserted as axioms, of which {pending} have an unverified proof)') print(f'search index -> {args.out_index}') if skipped: print(f'{len(skipped)} skipped for not being elaboration-checked: {", ".join(skipped)}') diff --git a/textbook/check_proofs.py b/textbook/check_proofs.py new file mode 100644 index 0000000..9290e06 --- /dev/null +++ b/textbook/check_proofs.py @@ -0,0 +1,127 @@ +"""Verify the database's proofs by compiling them, and record the verdict. + +check_statements.py asks "is this statement well-formed Lean"; this asks the much +stronger question "does this proof actually prove it". A database entry is only +allowed to claim proven status after passing here, so nothing enters the citable +premise library on an author's confidence alone. + +What counts as passing: + - `theorem : := by ` compiles with no error, and + - the proof text contains no `sorry`/`admit`/`native_decide`, and + - `#print axioms ` reports no axiom dependency beyond Lean's own three + (propext, Classical.choice, Quot.sound) -- in particular it must not lean on + `sorryAx`, nor on any of the book-asserted `axiom` declarations, since a + premise proven *through* an asserted axiom is not independently proven. + +With --update, entries that pass get `proof_checked: true` written back into the +database JSONL, which is what makes build_database.py emit them as real theorems +instead of axioms. Needs Lean/Lake and a built Mathlib, same as check_statements.py. +""" +import argparse +import json +import re +import subprocess +import tempfile +from dataclasses import dataclass +from pathlib import Path + +BANNED = re.compile(r'\b(sorry|admit|native_decide)\b') +# The three axioms Lean's own standard library is built on; anything else is ours. +ALLOWED_AXIOMS = {'propext', 'Classical.choice', 'Quot.sound'} +AXIOM_LINE = re.compile(r"^'[^']+' depends on axioms: \[(.*)\]$", re.M) + + +@dataclass +class ProofResult: + ok: bool + diagnostics: str + + +def check_proof(name, statement, proof, prelude='', command=None, cwd=None, timeout=120): + command = command or ['lean'] + if not proof or not proof.strip(): + return ProofResult(False, 'no proof recorded') + if BANNED.search(proof): + return ProofResult(False, f'proof uses a banned escape hatch: {BANNED.search(proof).group(1)}') + + body = '\n'.join(' ' + line for line in proof.strip().splitlines()) + source = ((prelude + '\n' if prelude else '') + + f'theorem {name} : {statement} := by\n{body}\n' + + f'#print axioms {name}\n') + + with tempfile.TemporaryDirectory(prefix='lean-proof-', dir=cwd) as directory: + path = Path(directory) / 'ProofCheck.lean' + path.write_text(source, encoding='utf-8') + try: + result = subprocess.run([*command, str(path)], cwd=cwd, capture_output=True, + text=True, timeout=timeout) + except subprocess.TimeoutExpired: + return ProofResult(False, 'Lean timeout') + + diagnostics = result.stdout + result.stderr + if result.returncode != 0 or 'error:' in diagnostics: + return ProofResult(False, diagnostics[-8000:]) + + match = AXIOM_LINE.search(diagnostics) + if match: + used = {a.strip() for a in match.group(1).split(',') if a.strip()} + extra = used - ALLOWED_AXIOMS + if extra: + return ProofResult(False, f'proof depends on non-standard axioms: {sorted(extra)}\n' + + diagnostics[-2000:]) + return ProofResult(True, diagnostics[-2000:]) + + +def main(): + parser = argparse.ArgumentParser(description='Compile and verify the proofs recorded in a database JSONL') + parser.add_argument('database', type=Path, help='e.g. database/goodman-1.6.jsonl') + parser.add_argument('--lean-command', default='["lean"]', help='JSON argv array; e.g. ["lake","env","lean"]') + parser.add_argument('--lean-project', help='Lean/Lake project working directory (needs Mathlib built)') + parser.add_argument('--timeout', type=float, default=120) + parser.add_argument('--report', type=Path, help='write JSONL of {id, ok, diagnostics} here') + parser.add_argument('--update', action='store_true', + help='write proof_checked back into the database for entries that pass') + parser.add_argument('--only', nargs='*', help='check only these ids') + args = parser.parse_args() + + command = json.loads(args.lean_command) + records = [json.loads(line) for line in args.database.read_text(encoding='utf-8').splitlines() if line.strip()] + + reports, checked, failed, skipped = [], 0, 0, 0 + for record in records: + if args.only and record['id'] not in args.only: + continue + if not record.get('proof'): + skipped += 1 + continue + name = record['id'].replace('-', '_') + result = check_proof(name, record['statement'], record['proof'], record.get('prelude', ''), + command, args.lean_project, args.timeout) + reports.append({"id": record['id'], "ok": result.ok, "diagnostics": result.diagnostics}) + print(('PROVED ' if result.ok else 'FAILED ') + record['id']) + if result.ok: + checked += 1 + if args.update: + record['proof_checked'] = True + else: + failed += 1 + if args.update: + record['proof_checked'] = False + + if args.update: + with args.database.open('w', encoding='utf-8') as stream: + for record in records: + stream.write(json.dumps(record, ensure_ascii=False) + '\n') + print(f'updated proof_checked in {args.database}') + + if args.report: + with args.report.open('w', encoding='utf-8') as stream: + for report in reports: + stream.write(json.dumps(report, ensure_ascii=False) + '\n') + + print(f'{checked} proved, {failed} failed, {skipped} entries have no proof recorded yet') + raise SystemExit(1 if failed else 0) + + +if __name__ == '__main__': + main() diff --git a/textbook/goodman-1.6.excluded.jsonl b/textbook/goodman-1.6.excluded.jsonl new file mode 100644 index 0000000..e69de29