From 1bbf018665422f7350e2779ce88de44d7dc973f7 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 21 Sep 2026 20:41:48 +0000 Subject: [PATCH 01/11] Update Lean toolchain and Mathlib to v4.28.0 No source changes were required; all 672 statements build unmodified. --- lean4/lake-manifest.json | 24 ++++++++++++------------ lean4/lakefile.lean | 2 +- lean4/lean-toolchain | 2 +- 3 files changed, 14 insertions(+), 14 deletions(-) diff --git a/lean4/lake-manifest.json b/lean4/lake-manifest.json index 4895731..d7dd85a 100644 --- a/lean4/lake-manifest.json +++ b/lean4/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "", - "rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900", + "rev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0", + "inputRev": "v4.28.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "009dc1e6f2feb2c96c081537d80a0905b2c6498f", + "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8f497d55985a189cea8020d9dc51260af1e41ad2", + "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,17 +45,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c04225ee7c0585effbd933662b3151f01b600e40", + "rev": "be3b2e63b1bbf496c478cef98b86972a37c1417d", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.85", + "inputRev": "v0.0.87", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d", + "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c", + "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a", + "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "55c37290ff6186e2e965d68cf853a57c0702db82", + "rev": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0", + "inputRev": "v4.28.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "putnam", diff --git a/lean4/lakefile.lean b/lean4/lakefile.lean index 63a6aa2..6e957c9 100644 --- a/lean4/lakefile.lean +++ b/lean4/lakefile.lean @@ -6,7 +6,7 @@ package «putnam» where leanOptions := #[ ⟨`autoImplicit, false⟩ ] -require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.27.0" +require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.28.0" @[default_target] lean_lib «putnam» where diff --git a/lean4/lean-toolchain b/lean4/lean-toolchain index 2bb276a..ea6ca7f 100644 --- a/lean4/lean-toolchain +++ b/lean4/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.27.0 \ No newline at end of file +leanprover/lean4:v4.28.0 \ No newline at end of file From 9b3d278b255541e6b8f560afbeb2123ddd02f64b Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 21 Sep 2026 20:50:00 +0000 Subject: [PATCH 02/11] Update Lean toolchain and Mathlib to v4.28.1 No source changes were required; all 672 statements build unmodified. --- lean4/lake-manifest.json | 8 ++++---- lean4/lakefile.lean | 2 +- lean4/lean-toolchain | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/lean4/lake-manifest.json b/lean4/lake-manifest.json index d7dd85a..31a8daa 100644 --- a/lean4/lake-manifest.json +++ b/lean4/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365", + "rev": "1f9fffd5ff0b854b8a1f1f69adc11c61f05f2515", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.28.0", + "inputRev": "v4.28.1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", @@ -45,10 +45,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "be3b2e63b1bbf496c478cef98b86972a37c1417d", + "rev": "b4cc9b4d5238886d01401dca9a9148bd3d00611a", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.87", + "inputRev": "v0.0.87+lean-v4.28.1", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", diff --git a/lean4/lakefile.lean b/lean4/lakefile.lean index 6e957c9..c802a5d 100644 --- a/lean4/lakefile.lean +++ b/lean4/lakefile.lean @@ -6,7 +6,7 @@ package «putnam» where leanOptions := #[ ⟨`autoImplicit, false⟩ ] -require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.28.0" +require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.28.1" @[default_target] lean_lib «putnam» where diff --git a/lean4/lean-toolchain b/lean4/lean-toolchain index ea6ca7f..2df487e 100644 --- a/lean4/lean-toolchain +++ b/lean4/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.28.0 \ No newline at end of file +leanprover/lean4:v4.28.1 \ No newline at end of file From fa438c26d67f86c789cebb3fe6bebea4a7bc3900 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 21 Sep 2026 20:57:56 +0000 Subject: [PATCH 03/11] Update Lean toolchain and Mathlib to v4.29.0 No source changes were required; all 672 statements build unmodified. --- lean4/lake-manifest.json | 22 +++++++++++----------- lean4/lakefile.lean | 2 +- lean4/lean-toolchain | 2 +- 3 files changed, 13 insertions(+), 13 deletions(-) diff --git a/lean4/lake-manifest.json b/lean4/lake-manifest.json index 31a8daa..1a738ab 100644 --- a/lean4/lake-manifest.json +++ b/lean4/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "", - "rev": "1f9fffd5ff0b854b8a1f1f69adc11c61f05f2515", + "rev": "8a178386ffc0f5fef0b77738bb5449d50efeea95", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.28.1", + "inputRev": "v4.29.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3", + "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e", + "rev": "48d5698bc464786347c1b0d859b18f938420f060", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,17 +45,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b4cc9b4d5238886d01401dca9a9148bd3d00611a", + "rev": "3c52dee17f0cd89c1ec14de78920d1bdaa3d26b3", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.87+lean-v4.28.1", + "inputRev": "v0.0.95", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1", + "rev": "7152850e7b216a0d409701617721b6e469d34bf6", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3", + "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f", + "rev": "756e3321fd3b02a85ffda19fef789916223e578c", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e", + "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.28.0", + "inputRev": "v4.29.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "putnam", diff --git a/lean4/lakefile.lean b/lean4/lakefile.lean index c802a5d..8d78acb 100644 --- a/lean4/lakefile.lean +++ b/lean4/lakefile.lean @@ -6,7 +6,7 @@ package «putnam» where leanOptions := #[ ⟨`autoImplicit, false⟩ ] -require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.28.1" +require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.29.0" @[default_target] lean_lib «putnam» where diff --git a/lean4/lean-toolchain b/lean4/lean-toolchain index 2df487e..d324cad 100644 --- a/lean4/lean-toolchain +++ b/lean4/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.28.1 \ No newline at end of file +leanprover/lean4:v4.29.0 \ No newline at end of file From a77c6c8bb17994bfa1be41d852f73f37eb5da3e3 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 21 Sep 2026 21:05:18 +0000 Subject: [PATCH 04/11] Update Lean toolchain and Mathlib to v4.29.1 No source changes were required; all 672 statements build unmodified. --- lean4/lake-manifest.json | 8 ++++---- lean4/lakefile.lean | 2 +- lean4/lean-toolchain | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/lean4/lake-manifest.json b/lean4/lake-manifest.json index 1a738ab..8f3e9e5 100644 --- a/lean4/lake-manifest.json +++ b/lean4/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "8a178386ffc0f5fef0b77738bb5449d50efeea95", + "rev": "5e932f97dd25535344f80f9dd8da3aab83df0fe6", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0", + "inputRev": "v4.29.1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", @@ -45,10 +45,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3c52dee17f0cd89c1ec14de78920d1bdaa3d26b3", + "rev": "4dd0959c44d1af0462bd604d0f87c5781307d709", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.95", + "inputRev": "v0.0.95+lean-v4.29.1", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", diff --git a/lean4/lakefile.lean b/lean4/lakefile.lean index 8d78acb..6354ec8 100644 --- a/lean4/lakefile.lean +++ b/lean4/lakefile.lean @@ -6,7 +6,7 @@ package «putnam» where leanOptions := #[ ⟨`autoImplicit, false⟩ ] -require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.29.0" +require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.29.1" @[default_target] lean_lib «putnam» where diff --git a/lean4/lean-toolchain b/lean4/lean-toolchain index d324cad..05a063a 100644 --- a/lean4/lean-toolchain +++ b/lean4/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0 \ No newline at end of file +leanprover/lean4:v4.29.1 \ No newline at end of file From 34387b8b9d866d67ea90351156e75d33aef22dbd Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 21 Sep 2026 21:14:49 +0000 Subject: [PATCH 05/11] Update Lean toolchain and Mathlib to v4.30.0 Finset is now SetLike and Finset.toSet was removed, so putnam_1966_b5 uses the Finset-to-Set coercion instead. An explicit Set ascription is needed because Collinear's point type is otherwise an unresolved metavariable. --- lean4/lake-manifest.json | 31 ++++++++++++++++--------------- lean4/lakefile.lean | 2 +- lean4/lean-toolchain | 2 +- lean4/src/putnam_1966_b5.lean | 2 +- 4 files changed, 19 insertions(+), 18 deletions(-) diff --git a/lean4/lake-manifest.json b/lean4/lake-manifest.json index 8f3e9e5..efecbf8 100644 --- a/lean4/lake-manifest.json +++ b/lean4/lake-manifest.json @@ -1,21 +1,21 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "", - "rev": "5e932f97dd25535344f80f9dd8da3aab83df0fe6", + "rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.1", + "inputRev": "v4.30.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3", + "rev": "a456461b368b71d2accd95234832cd9c174b5437", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "48d5698bc464786347c1b0d859b18f938420f060", + "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,37 +45,37 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4dd0959c44d1af0462bd604d0f87c5781307d709", + "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.95+lean-v4.29.1", + "inputRev": "v0.0.99", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7152850e7b216a0d409701617721b6e469d34bf6", + "rev": "558915ae105bfd8074e22d597613d1961822adc2", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.30.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d", + "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.30.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "756e3321fd3b02a85ffda19fef789916223e578c", + "rev": "32dc18cde3684679f3c003de608743b57498c56f", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,11 +85,12 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29", + "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0", + "inputRev": "v4.30.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "putnam", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lean4/lakefile.lean b/lean4/lakefile.lean index 6354ec8..989f8cb 100644 --- a/lean4/lakefile.lean +++ b/lean4/lakefile.lean @@ -6,7 +6,7 @@ package «putnam» where leanOptions := #[ ⟨`autoImplicit, false⟩ ] -require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.29.1" +require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.30.0" @[default_target] lean_lib «putnam» where diff --git a/lean4/lean-toolchain b/lean4/lean-toolchain index 05a063a..5a8f161 100644 --- a/lean4/lean-toolchain +++ b/lean4/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.1 \ No newline at end of file +leanprover/lean4:v4.30.0 \ No newline at end of file diff --git a/lean4/src/putnam_1966_b5.lean b/lean4/src/putnam_1966_b5.lean index ae0894e..2dba3d2 100644 --- a/lean4/src/putnam_1966_b5.lean +++ b/lean4/src/putnam_1966_b5.lean @@ -8,7 +8,7 @@ Prove that any set of $n \ge 3$ distinct points in the Euclidean plane, no three theorem putnam_1966_b5 (S : Finset (EuclideanSpace ℝ (Fin 2))) (hcard : S.card ≥ 3) -(hS : ∀ s ⊆ S, s.card = 3 → ¬Collinear ℝ s.toSet) +(hS : ∀ s ⊆ S, s.card = 3 → ¬Collinear ℝ (s : Set (EuclideanSpace ℝ (Fin 2)))) : ∃ L : ZMod S.card → (EuclideanSpace ℝ (Fin 2)), (∀ p ∈ S, ∃! i : ZMod S.card, p = L i) ∧ ∀ i j : ZMod S.card, i ≠ j → (∀ I : EuclideanSpace ℝ (Fin 2), (I ∈ segment ℝ (L i) (L (i + 1)) ∧ I ∈ segment ℝ (L j) (L (j + 1))) → From 096d3b93be374ff74cc12116b9a14cc14e7ce315 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 21 Sep 2026 21:23:41 +0000 Subject: [PATCH 06/11] Update Lean toolchain and Mathlib to v4.31.0 Lean 4.31 is stricter about position-sensitive parsing of declaration signatures: a continuation line at column 0 with no brackets open is no longer treated as part of the preceding application. Indented the continuation line in putnam_1976_b1 (whitespace only, statement unchanged). --- lean4/lake-manifest.json | 26 +++++++++++++------------- lean4/lakefile.lean | 2 +- lean4/lean-toolchain | 2 +- lean4/src/putnam_1976_b1.lean | 2 +- 4 files changed, 16 insertions(+), 16 deletions(-) diff --git a/lean4/lake-manifest.json b/lean4/lake-manifest.json index efecbf8..a6ce4d6 100644 --- a/lean4/lake-manifest.json +++ b/lean4/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "", - "rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f", + "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0", + "inputRev": "v4.31.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a456461b368b71d2accd95234832cd9c174b5437", + "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1", + "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,37 +45,37 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8", + "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.99", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "558915ae105bfd8074e22d597613d1961822adc2", + "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c", + "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "32dc18cde3684679f3c003de608743b57498c56f", + "rev": "fa08db58b30eb033edcdab331bba000827f9f785", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c", + "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0", + "inputRev": "v4.31.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "putnam", diff --git a/lean4/lakefile.lean b/lean4/lakefile.lean index 989f8cb..bc0f4a3 100644 --- a/lean4/lakefile.lean +++ b/lean4/lakefile.lean @@ -6,7 +6,7 @@ package «putnam» where leanOptions := #[ ⟨`autoImplicit, false⟩ ] -require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.30.0" +require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.31.0" @[default_target] lean_lib «putnam» where diff --git a/lean4/lean-toolchain b/lean4/lean-toolchain index 5a8f161..133a3f7 100644 --- a/lean4/lean-toolchain +++ b/lean4/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.30.0 \ No newline at end of file +leanprover/lean4:v4.31.0 \ No newline at end of file diff --git a/lean4/src/putnam_1976_b1.lean b/lean4/src/putnam_1976_b1.lean index ef96553..6a687bc 100644 --- a/lean4/src/putnam_1976_b1.lean +++ b/lean4/src/putnam_1976_b1.lean @@ -9,5 +9,5 @@ Find $$\lim_{n \to \infty} \frac{1}{n} \sum_{k=1}^{n}\left(\left\lfloor \frac{2n -/ theorem putnam_1976_b1 : Tendsto (fun n : ℕ => ((1 : ℝ)/n)*∑ k ∈ Finset.Icc (1 : ℤ) n, (Int.floor ((2*n)/k) - 2*Int.floor (n/k))) atTop -(𝓝 (Real.log putnam_1976_b1_solution.1 - putnam_1976_b1_solution.2)) := + (𝓝 (Real.log putnam_1976_b1_solution.1 - putnam_1976_b1_solution.2)) := sorry From aadab5305387dda2f59a60aea630166428ed7c16 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 21 Sep 2026 21:30:46 +0000 Subject: [PATCH 07/11] Update Lean toolchain and Mathlib to v4.32.0 No source changes were required; all 672 statements build unmodified. --- lean4/lake-manifest.json | 20 ++++++++++---------- lean4/lakefile.lean | 2 +- lean4/lean-toolchain | 2 +- 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/lean4/lake-manifest.json b/lean4/lake-manifest.json index a6ce4d6..d38a7a2 100644 --- a/lean4/lake-manifest.json +++ b/lean4/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "", - "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f", + "rev": "81a5d257c8e410db227a6665ed08f64fea08e997", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0", + "inputRev": "v4.32.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc", + "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d", + "rev": "7e9612bf0b9ee66db3cb5b9988a35afc706f5a12", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9", + "rev": "6e311e2a844da9b2cc3971187df2fe0066947b93", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f", + "rev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2", + "rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fa08db58b30eb033edcdab331bba000827f9f785", + "rev": "023ce7d62a0531e22a5331e20b587817a80d49ff", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c", + "rev": "88679d088c9720c27ebdf2ba4dafe17341747f94", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0", + "inputRev": "v4.32.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "putnam", diff --git a/lean4/lakefile.lean b/lean4/lakefile.lean index bc0f4a3..9d7f89c 100644 --- a/lean4/lakefile.lean +++ b/lean4/lakefile.lean @@ -6,7 +6,7 @@ package «putnam» where leanOptions := #[ ⟨`autoImplicit, false⟩ ] -require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.31.0" +require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.32.0" @[default_target] lean_lib «putnam» where diff --git a/lean4/lean-toolchain b/lean4/lean-toolchain index 133a3f7..2544c30 100644 --- a/lean4/lean-toolchain +++ b/lean4/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.31.0 \ No newline at end of file +leanprover/lean4:v4.32.0 \ No newline at end of file From a1f3fd9ea9ad1fe30aa055ac601a7a148f33003e Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 21 Sep 2026 21:38:27 +0000 Subject: [PATCH 08/11] Update Lean toolchain and Mathlib to v4.32.1 No source changes were required; all 672 statements build unmodified. --- lean4/lake-manifest.json | 4 ++-- lean4/lakefile.lean | 2 +- lean4/lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lean4/lake-manifest.json b/lean4/lake-manifest.json index d38a7a2..4f29094 100644 --- a/lean4/lake-manifest.json +++ b/lean4/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "81a5d257c8e410db227a6665ed08f64fea08e997", + "rev": "520045ab14e26149ee970e2e617ca04b09bde5d6", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.32.0", + "inputRev": "v4.32.1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", diff --git a/lean4/lakefile.lean b/lean4/lakefile.lean index 9d7f89c..91a5c7a 100644 --- a/lean4/lakefile.lean +++ b/lean4/lakefile.lean @@ -6,7 +6,7 @@ package «putnam» where leanOptions := #[ ⟨`autoImplicit, false⟩ ] -require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.32.0" +require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.32.1" @[default_target] lean_lib «putnam» where diff --git a/lean4/lean-toolchain b/lean4/lean-toolchain index 2544c30..e29f71d 100644 --- a/lean4/lean-toolchain +++ b/lean4/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.32.0 \ No newline at end of file +leanprover/lean4:v4.32.1 \ No newline at end of file From 875229ccd07aed7ed277871c0f45164bb9d9dcfd Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 21 Sep 2026 21:45:56 +0000 Subject: [PATCH 09/11] Update Lean toolchain and Mathlib to v4.32.2 No source changes were required; all 672 statements build unmodified. --- lean4/lake-manifest.json | 4 ++-- lean4/lakefile.lean | 2 +- lean4/lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lean4/lake-manifest.json b/lean4/lake-manifest.json index 4f29094..dba7867 100644 --- a/lean4/lake-manifest.json +++ b/lean4/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "520045ab14e26149ee970e2e617ca04b09bde5d6", + "rev": "905b95818eb32af7874a58b427f50c1711a5e96c", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.32.1", + "inputRev": "v4.32.2", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", diff --git a/lean4/lakefile.lean b/lean4/lakefile.lean index 91a5c7a..c66ea2b 100644 --- a/lean4/lakefile.lean +++ b/lean4/lakefile.lean @@ -6,7 +6,7 @@ package «putnam» where leanOptions := #[ ⟨`autoImplicit, false⟩ ] -require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.32.1" +require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.32.2" @[default_target] lean_lib «putnam» where diff --git a/lean4/lean-toolchain b/lean4/lean-toolchain index e29f71d..cd7198b 100644 --- a/lean4/lean-toolchain +++ b/lean4/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.32.1 \ No newline at end of file +leanprover/lean4:v4.32.2 \ No newline at end of file From 13d042960189f55d748048317c24064a0e2215ea Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 21 Sep 2026 21:53:54 +0000 Subject: [PATCH 10/11] Update Lean toolchain and Mathlib to v4.33.0 No source changes were required; all 672 statements build unmodified. --- lean4/lake-manifest.json | 22 +++++++++++----------- lean4/lakefile.lean | 2 +- lean4/lean-toolchain | 2 +- 3 files changed, 13 insertions(+), 13 deletions(-) diff --git a/lean4/lake-manifest.json b/lean4/lake-manifest.json index dba7867..58d23bf 100644 --- a/lean4/lake-manifest.json +++ b/lean4/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "", - "rev": "905b95818eb32af7874a58b427f50c1711a5e96c", + "rev": "db584cd6d46c92f209a44c0f1c829460d327499d", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.32.2", + "inputRev": "v4.33.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62", + "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7e9612bf0b9ee66db3cb5b9988a35afc706f5a12", + "rev": "16f02aa7642864af59f1ff0e384a015994db9118", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6e311e2a844da9b2cc3971187df2fe0066947b93", + "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3", + "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc", + "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "023ce7d62a0531e22a5331e20b587817a80d49ff", + "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "88679d088c9720c27ebdf2ba4dafe17341747f94", + "rev": "6130a47896ce867c6a4a55373441e59e565bad0f", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.32.0", + "inputRev": "v4.33.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "putnam", diff --git a/lean4/lakefile.lean b/lean4/lakefile.lean index c66ea2b..15d8d24 100644 --- a/lean4/lakefile.lean +++ b/lean4/lakefile.lean @@ -6,7 +6,7 @@ package «putnam» where leanOptions := #[ ⟨`autoImplicit, false⟩ ] -require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.32.2" +require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.33.0" @[default_target] lean_lib «putnam» where diff --git a/lean4/lean-toolchain b/lean4/lean-toolchain index cd7198b..6a884ba 100644 --- a/lean4/lean-toolchain +++ b/lean4/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.32.2 \ No newline at end of file +leanprover/lean4:v4.33.0 \ No newline at end of file From b89ee5b2fde004fef4a4081298c78b23d1927dca Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 21 Sep 2026 22:01:34 +0000 Subject: [PATCH 11/11] Update Lean toolchain and Mathlib to v4.33.1 No source changes were required; all 672 statements build unmodified. --- lean4/lake-manifest.json | 4 ++-- lean4/lakefile.lean | 2 +- lean4/lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lean4/lake-manifest.json b/lean4/lake-manifest.json index 58d23bf..69450ef 100644 --- a/lean4/lake-manifest.json +++ b/lean4/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "db584cd6d46c92f209a44c0f1c829460d327499d", + "rev": "0df444a360eaa60ab8c11dca51a86af692955474", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0", + "inputRev": "v4.33.1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", diff --git a/lean4/lakefile.lean b/lean4/lakefile.lean index 15d8d24..c8930a2 100644 --- a/lean4/lakefile.lean +++ b/lean4/lakefile.lean @@ -6,7 +6,7 @@ package «putnam» where leanOptions := #[ ⟨`autoImplicit, false⟩ ] -require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.33.0" +require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.33.1" @[default_target] lean_lib «putnam» where diff --git a/lean4/lean-toolchain b/lean4/lean-toolchain index 6a884ba..3859d96 100644 --- a/lean4/lean-toolchain +++ b/lean4/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.0 \ No newline at end of file +leanprover/lean4:v4.33.1 \ No newline at end of file