From d96c59d8f6e9ee361b81563c7142fe48ca148e88 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 12 Aug 2024 09:52:31 +0000 Subject: [PATCH 1/3] Update Lean and Mathlib to v4.8.0 --- lean4/lake-manifest.json | 26 +++++++++++++------------- lean4/lakefile.lean | 2 +- lean4/lean-toolchain | 2 +- lean4/src/putnam_2001_a5.lean | 2 +- 4 files changed, 16 insertions(+), 16 deletions(-) diff --git a/lean4/lake-manifest.json b/lean4/lake-manifest.json index 1c07794b..5b7b4298 100644 --- a/lean4/lake-manifest.json +++ b/lean4/lake-manifest.json @@ -1,11 +1,11 @@ {"version": 7, "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/std4", + [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a", - "name": "std", + "rev": "551ff2d7dffd7af914cdbd01abbd449fe3e3d428", + "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, @@ -13,7 +13,7 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "64365c656d5e1bffa127d2a1795f471529ee0178", + "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -22,25 +22,25 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79", + "rev": "53ba96ad7666d4a2515292974631629b5ea5dfee", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8", + "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.30", + "inputRev": "v0.0.36", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5", + "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -49,19 +49,19 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662", + "rev": "77e081815b30b0d30707e1c5b0c6a6761f7a2404", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, - "rev": "a45ae63747140c1b2cbad9d46f518015c047047a", + "rev": "b5eba595428809e96f3ed113bc7ba776c5f801ac", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.7.0", + "inputRev": "v4.8.0", "inherited": false, "configFile": "lakefile.lean"}], "name": "putnam", diff --git a/lean4/lakefile.lean b/lean4/lakefile.lean index 4e2adab7..8a715701 100644 --- a/lean4/lakefile.lean +++ b/lean4/lakefile.lean @@ -3,7 +3,7 @@ open Lake DSL package «putnam» where -- add package configuration options here -require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.7.0" +require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.8.0" @[default_target] lean_lib «putnam» where diff --git a/lean4/lean-toolchain b/lean4/lean-toolchain index 9ad30404..ef1f67e9 100644 --- a/lean4/lean-toolchain +++ b/lean4/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.7.0 +leanprover/lean4:v4.8.0 diff --git a/lean4/src/putnam_2001_a5.lean b/lean4/src/putnam_2001_a5.lean index 66bc7a28..d82ea63a 100644 --- a/lean4/src/putnam_2001_a5.lean +++ b/lean4/src/putnam_2001_a5.lean @@ -4,5 +4,5 @@ open BigOperators open Topology Filter Polynomial Set theorem putnam_2001_a5 -: ∃! (a : ℤ) (n : ℕ), a > 0 ∧ n > 0 ∧ a^(n+1) - (a+1)^n = 2001 := +: ∃! an : ℤ × ℕ, let (a, n) := an; a > 0 ∧ n > 0 ∧ a^(n+1) - (a+1)^n = 2001 := sorry From b867bc72d6d725b48ae3a27d540a0b78e1c7d6f3 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 12 Aug 2024 10:32:15 +0000 Subject: [PATCH 2/3] Update Lean and Mathlib to v4.9.0 --- lean4/lake-manifest.json | 18 +++++++++--------- lean4/lakefile.lean | 2 +- lean4/lean-toolchain | 2 +- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/lean4/lake-manifest.json b/lean4/lake-manifest.json index 5b7b4298..82fe232c 100644 --- a/lean4/lake-manifest.json +++ b/lean4/lake-manifest.json @@ -1,10 +1,10 @@ -{"version": 7, +{"version": "1.0.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "551ff2d7dffd7af914cdbd01abbd449fe3e3d428", + "rev": "54bb04c3119f24fde14b9068c4b2e69db52a1450", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -13,7 +13,7 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6", + "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "53ba96ad7666d4a2515292974631629b5ea5dfee", + "rev": "06cca4bd36b2af743d4858c5cc31604aa9da26bc", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -31,10 +31,10 @@ {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5", + "rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.36", + "inputRev": "v0.0.38", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "77e081815b30b0d30707e1c5b0c6a6761f7a2404", + "rev": "c29c3cdce415240e9dcec5c583ad5d36f83f9c71", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,10 +58,10 @@ {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, - "rev": "b5eba595428809e96f3ed113bc7ba776c5f801ac", + "rev": "f0957a7575317490107578ebaee9efaf8e62a4ab", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.8.0", + "inputRev": "v4.9.0", "inherited": false, "configFile": "lakefile.lean"}], "name": "putnam", diff --git a/lean4/lakefile.lean b/lean4/lakefile.lean index 8a715701..c72ea23d 100644 --- a/lean4/lakefile.lean +++ b/lean4/lakefile.lean @@ -3,7 +3,7 @@ open Lake DSL package «putnam» where -- add package configuration options here -require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.8.0" +require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.9.0" @[default_target] lean_lib «putnam» where diff --git a/lean4/lean-toolchain b/lean4/lean-toolchain index ef1f67e9..4ef27c47 100644 --- a/lean4/lean-toolchain +++ b/lean4/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.8.0 +leanprover/lean4:v4.9.0 From cf8d5d575feefe75fede144f5696f922ecbac83e Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 12 Aug 2024 12:39:07 +0000 Subject: [PATCH 3/3] Update Lean and Mathlib to v4.10.0 --- lean4/lake-manifest.json | 31 +++++++++++++++++++------------ lean4/lakefile.lean | 2 +- lean4/lean-toolchain | 2 +- lean4/src/putnam_2018_b1.lean | 16 ++++++++-------- 4 files changed, 29 insertions(+), 22 deletions(-) diff --git a/lean4/lake-manifest.json b/lean4/lake-manifest.json index 82fe232c..f22bba95 100644 --- a/lean4/lake-manifest.json +++ b/lean4/lake-manifest.json @@ -1,10 +1,11 @@ -{"version": "1.0.0", +{"version": "1.1.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "54bb04c3119f24fde14b9068c4b2e69db52a1450", + "scope": "leanprover-community", + "rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -13,7 +14,8 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6", + "scope": "leanprover-community", + "rev": "01ad33937acd996ee99eb74eefb39845e4e4b9f5", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -22,7 +24,8 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "06cca4bd36b2af743d4858c5cc31604aa9da26bc", + "scope": "leanprover-community", + "rev": "209712c78b16c795453b6da7f7adbda4589a8f21", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -31,25 +34,28 @@ {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9", + "scope": "leanprover-community", + "rev": "c87908619cccadda23f71262e6898b9893bffa36", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.38", + "inputRev": "v0.0.40", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", + "scope": "", + "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/import-graph.git", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, - "rev": "c29c3cdce415240e9dcec5c583ad5d36f83f9c71", + "scope": "leanprover-community", + "rev": "543725b3bfed792097fc134adca628406f6145f5", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,10 +64,11 @@ {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, - "rev": "f0957a7575317490107578ebaee9efaf8e62a4ab", + "scope": "", + "rev": "a719ba5c3115d47b68bf0497a9dd1bcbb21ea663", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.9.0", + "inputRev": "v4.10.0", "inherited": false, "configFile": "lakefile.lean"}], "name": "putnam", diff --git a/lean4/lakefile.lean b/lean4/lakefile.lean index c72ea23d..abf5441a 100644 --- a/lean4/lakefile.lean +++ b/lean4/lakefile.lean @@ -3,7 +3,7 @@ open Lake DSL package «putnam» where -- add package configuration options here -require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.9.0" +require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.10.0" @[default_target] lean_lib «putnam» where diff --git a/lean4/lean-toolchain b/lean4/lean-toolchain index 4ef27c47..7f0ea50a 100644 --- a/lean4/lean-toolchain +++ b/lean4/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.9.0 +leanprover/lean4:v4.10.0 diff --git a/lean4/src/putnam_2018_b1.lean b/lean4/src/putnam_2018_b1.lean index 66a3d3c0..97407b02 100644 --- a/lean4/src/putnam_2018_b1.lean +++ b/lean4/src/putnam_2018_b1.lean @@ -1,17 +1,17 @@ import Mathlib open BigOperators -abbrev putnam_2018_b1_solution : Set (Vector ℤ 2) := sorry --- {v : Vector ℤ 2 | ∃ b : ℤ, 0 ≤ b ∧ b ≤ 100 ∧ Even b ∧ v.toList = [1, b]} +abbrev putnam_2018_b1_solution : Set (Mathlib.Vector ℤ 2) := sorry +-- {v : Mathlib.Vector ℤ 2 | ∃ b : ℤ, 0 ≤ b ∧ b ≤ 100 ∧ Even b ∧ v.toList = [1, b]} theorem putnam_2018_b1 -(P : Finset (Vector ℤ 2)) -(v : Vector ℤ 2) +(P : Finset (Mathlib.Vector ℤ 2)) +(v : Mathlib.Vector ℤ 2) (vinP : Prop) -(Pvdiff : Finset (Vector ℤ 2)) +(Pvdiff : Finset (Mathlib.Vector ℤ 2)) (Pvpart : Prop) -(hP : P = {v' : Vector ℤ 2 | 0 ≤ v'[0] ∧ v'[0] ≤ 2 ∧ 0 ≤ v'[1] ∧ v'[1] ≤ 100}) +(hP : P = {v' : Mathlib.Vector ℤ 2 | 0 ≤ v'[0] ∧ v'[0] ≤ 2 ∧ 0 ≤ v'[1] ∧ v'[1] ≤ 100}) (hvinP : vinP = (v ∈ P)) -(hPvdiff : Pvdiff = P \ ({v} : Finset (Vector ℤ 2))) -(hPvpart : Pvpart = (∃ Q R : Finset (Vector ℤ 2), (Q ∪ R = Pvdiff) ∧ (Q ∩ R = ∅) ∧ (Q.card = R.card) ∧ (∑ q in Q, q[0] = ∑ r in R, r[0]) ∧ (∑ q in Q, q[1] = ∑ r in R, r[1]))) +(hPvdiff : Pvdiff = P \ ({v} : Finset (Mathlib.Vector ℤ 2))) +(hPvpart : Pvpart = (∃ Q R : Finset (Mathlib.Vector ℤ 2), (Q ∪ R = Pvdiff) ∧ (Q ∩ R = ∅) ∧ (Q.card = R.card) ∧ (∑ q in Q, q[0] = ∑ r in R, r[0]) ∧ (∑ q in Q, q[1] = ∑ r in R, r[1]))) : (vinP ∧ Pvpart) ↔ v ∈ putnam_2018_b1_solution := sorry