leanprover · kim-em · Sep 16, 2026 · Sep 16, 2026 · Sep 16, 2026 · Sep 16, 2026
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -213,9 +213,9 @@ jobs:
           set -euo pipefail
           git clone https://github.com/leanprover/lean4export.git .ci/lean4export
           cd .ci/lean4export
-          # lean4export pinned to 15f6055e (= refs/tags/v4.33.0 as of 2026-08-14).
+          # lean4export pinned to 076e8e57 (= refs/tags/v4.34.0 as of 2026-09-16).
           # Bump procedure: SECURITY.md > "Bumping pinned dependencies".
-          git checkout 15f6055e299ad5b89345e533cc2192f4cc00f659  # pin-audit: exempt -- SHA, see comment
+          git checkout 076e8e57707e813375e8f9da8bf989799ace9680  # pin-audit: exempt -- SHA, see comment
           cp "$GITHUB_WORKSPACE/lean-toolchain" lean-toolchain
           lake build lean4export
           echo "$PWD/.lake/build/bin" >> "$GITHUB_PATH"
@@ -224,9 +224,9 @@ jobs:
         run: |
           git clone https://github.com/leanprover/comparator.git .ci/comparator
           cd .ci/comparator
-          # comparator pinned to 71b52ec2 (leanprover/comparator, originally adopted before 2026-05-04).
+          # comparator pinned to d03acab1 (= refs/tags/v4.34.0 as of 2026-09-16).
           # Bump procedure: SECURITY.md > "Bumping pinned dependencies".
-          git checkout 71b52ec29e06d4b7d882726553b1ceb99a2499e0  # pin-audit: exempt -- SHA, see comment
+          git checkout d03acab154d269c06e60e4de7e4cc85deebff94b  # pin-audit: exempt -- SHA, see comment
           lake build comparator
           echo "$PWD/.lake/build/bin" >> "$GITHUB_PATH"
 

diff --git a/LeanEval/AlgebraicGeometry/DirectSummand.lean b/LeanEval/AlgebraicGeometry/DirectSummand.lean
@@ -50,7 +50,7 @@ noncomputable def rightDerivedFunctorPlusUnit' {C D : Type*} [Category* C] [Cate
     F ⋙ DerivedCategory.Plus.singleFunctor _ n ⟶
     DerivedCategory.Plus.singleFunctor _ n ⋙ F.rightDerivedFunctorPlus :=
   Functor.whiskerRight (singleFunctorMapHomotopyCategoryPlus F n).inv DerivedCategory.Plus.Qh ≫
-    (HomotopyCategory.Plus.singleFunctor _ n).whiskerLeft F.rightDerivedFunctorPlusUnit
+    (HomotopyCategory.Plus.singleFunctor C n).whiskerLeft F.rightDerivedFunctorPlusUnith
 
 instance {C : Type*} [Category* C] {J : GrothendieckTopology C} (R : Sheaf J RingCat) (X : Cᵒᵖ) :
     (SheafOfModules.evaluation R X).Additive where

diff --git a/LeanEval/AlgebraicGeometry/MotivicInvariants.lean b/LeanEval/AlgebraicGeometry/MotivicInvariants.lean
@@ -7,7 +7,7 @@ Authors: Justus Springer
 import Mathlib.AlgebraicGeometry.Birational.Birational
 import Mathlib.AlgebraicGeometry.Birational.Composition
 import Mathlib.AlgebraicGeometry.Morphisms.Proper
-import Mathlib.Data.Complex.Basic
+import Mathlib.Basic.Complex.Basic
 import Mathlib.NumberTheory.NumberField.Basic
 import EvalTools.Markers
 

diff --git a/LeanEval/Combinatorics/PseudorandomGrassmann.lean b/LeanEval/Combinatorics/PseudorandomGrassmann.lean
@@ -7,7 +7,7 @@ Authors: Justus Springer
 import Mathlib.Algebra.Field.ZMod
 import Mathlib.Combinatorics.SimpleGraph.Density
 import Mathlib.Combinatorics.SimpleGraph.Finite
-import Mathlib.Data.Real.Basic
+import Mathlib.Basic.Real.Basic
 import Mathlib.Data.SetLike.Fintype
 import Mathlib.LinearAlgebra.Dimension.Finrank
 import Mathlib.Order.Filter.AtTopBot.Defs

diff --git a/LeanEval/ComplexAnalysis/ComplementaryPolynomials.lean b/LeanEval/ComplexAnalysis/ComplementaryPolynomials.lean
@@ -1,4 +1,5 @@
 import Mathlib.Algebra.Polynomial.Basic
+import Mathlib.Algebra.Polynomial.Degree.Defs
 import Mathlib.Analysis.Complex.Circle
 import EvalTools.Markers
 

diff --git a/LeanEval/Dynamics/PointwiseErgodicTheorems.lean b/LeanEval/Dynamics/PointwiseErgodicTheorems.lean
@@ -5,6 +5,7 @@ Authors: David Ledvinka
 -/
 
 import Mathlib.Analysis.Normed.Lp.PiLp
+import Mathlib.Algebra.Polynomial.Degree.Defs
 import Mathlib.MeasureTheory.Function.LpSpace.Basic
 import EvalTools.Markers
 

diff --git a/LeanEval/GameTheory/Nash.lean b/LeanEval/GameTheory/Nash.lean
@@ -14,8 +14,8 @@ equilibrium.
 Nash gave two proofs: the 1950 one uses Brouwer's fixed-point theorem; the
 1951 one uses Kakutani's set-valued generalization.
 
-mathlib has `stdSimplex ℝ S` (the natural model of a mixed strategy) and the
-standard finite-sum/product machinery, but **no game theory at all** —
+mathlib has the standard finite-sum/product machinery needed to describe the standard simplex,
+but **no game theory at all** —
 there is no `Mathlib/GameTheory/` module, and `grep -ri nash`,
 `mixed.strategy`, `best.response` returns nothing relevant. No formalization
 of Nash equilibrium existence was found in any major proof assistant.
@@ -25,7 +25,8 @@ open Set Function
 
 /-- A **mixed strategy** for a player with finite pure-strategy set `S` is a
 probability distribution on `S`: a non-negative function summing to `1`. -/
-abbrev MixedStrategy (S : Type*) [Fintype S] : Set (S → ℝ) := stdSimplex ℝ S
+abbrev MixedStrategy (S : Type*) [Fintype S] : Set (S → ℝ) :=
+  { f | (∀ x, 0 ≤ f x) ∧ ∑ x, f x = 1 }
 
 /-- A **strategy profile** is a tuple assigning each of the `n` players a
 pure strategy from their own set. -/

diff --git a/LeanEval/Geometry/SymplecticMonodromy.lean b/LeanEval/Geometry/SymplecticMonodromy.lean
@@ -28,7 +28,7 @@ open MvPowerSeries
 
 /-- The Milnor number of `f` is `dim_ℂ ℂ⟦z₁, ⋯, zₙ⟧ / ⟨∂f/∂z₁, ⋯, ∂f/∂zₙ⟩`. -/
 noncomputable def milnorNumber {σ R : Type*} [CommRing R] (f : MvPowerSeries σ R) : ℕ∞ :=
-  (Module.rank R (MvPowerSeries σ R ⧸ Ideal.span (Set.range (pderiv R · f)))).toENat
+  (Module.rank R (MvPowerSeries σ R ⧸ Ideal.span (Set.range (pderiv · f)))).toENat
 
 /--
 Statement of Theorem 1.1:

diff --git a/LeanEval/GroupTheory/OnPropertyT.lean b/LeanEval/GroupTheory/OnPropertyT.lean
@@ -6,7 +6,7 @@ Authors: Thomas Browning
 
 import Mathlib.Algebra.Group.Pointwise.Set.Basic
 import Mathlib.Algebra.MonoidAlgebra.MapDomain
-import Mathlib.Data.Real.Basic
+import Mathlib.Basic.Real.Basic
 import Mathlib.GroupTheory.FreeGroup.Basic
 import Mathlib.SetTheory.Cardinal.Finite
 import EvalTools.Markers

diff --git a/LeanEval/GroupTheory/OreConjecture.lean b/LeanEval/GroupTheory/OreConjecture.lean
@@ -1,4 +1,4 @@
-import Mathlib.Data.Finite.Defs
+import Mathlib.Basic.Finite.Defs
 import Mathlib.GroupTheory.Commutator.Basic
 import Mathlib.GroupTheory.Subgroup.Simple
 import EvalTools.Markers

diff --git a/LeanEval/NumberTheory/ZagierHoffmanPositiveChar.lean b/LeanEval/NumberTheory/ZagierHoffmanPositiveChar.lean
@@ -6,6 +6,7 @@ Authors: Katerina Hristova
 
 import Mathlib.NumberTheory.FunctionField
 import Mathlib.RingTheory.SimpleRing.Principal
+import Mathlib.Topology.Algebra.InfiniteSum.Defs
 import EvalTools.Markers
 
 /-!

diff --git a/LeanEval/RepresentationTheory/ExceptionalLieTensorSquare.lean b/LeanEval/RepresentationTheory/ExceptionalLieTensorSquare.lean
@@ -2,7 +2,7 @@ import Mathlib.Algebra.Lie.SerreConstruction
 import Mathlib.Algebra.Lie.TensorProduct
 import Mathlib.Algebra.Lie.UniversalEnveloping
 import Mathlib.Algebra.Lie.Semisimple.Defs
-import Mathlib.Data.Complex.Basic
+import Mathlib.Basic.Complex.Basic
 import Mathlib.LinearAlgebra.Dimension.Finrank
 import Mathlib.RingTheory.SimpleModule.Isotypic
 import EvalTools.Markers

diff --git a/LeanEval/RepresentationTheory/McKayConjecture.lean b/LeanEval/RepresentationTheory/McKayConjecture.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning
 -/
 
-import Mathlib.Data.Complex.Basic
+import Mathlib.Basic.Complex.Basic
 import Mathlib.GroupTheory.Sylow
 import Mathlib.RepresentationTheory.Character
 import EvalTools.Markers

diff --git a/README.md b/README.md
@@ -225,15 +225,15 @@ export PATH="$(go env GOPATH)/bin:$PATH"
 lean_eval_root="$(pwd)"  # run this setup from the lean-eval repository root
 git clone https://github.com/leanprover/lean4export.git
 ( cd lean4export
-  git checkout 4e7915201d3f9f04470d9eae002fa695f7cdc589
+  git checkout 076e8e57707e813375e8f9da8bf989799ace9680
   cp "$lean_eval_root/lean-toolchain" lean-toolchain
   lake build lean4export )
 export PATH="$PWD/lean4export/.lake/build/bin:$PATH"
 
 # comparator — clone, check out the pin (adds `def`-hole support), and build.
 git clone https://github.com/leanprover/comparator.git
 ( cd comparator
-  git checkout 71b52ec29e06d4b7d882726553b1ceb99a2499e0
+  git checkout d03acab154d269c06e60e4de7e4cc85deebff94b
   lake build comparator )
 export PATH="$PWD/comparator/.lake/build/bin:$PATH"
 
@@ -249,7 +249,7 @@ export PATH="$PWD/nanoda_lib/target/release:$PATH"
 ```
 
 `lean4export` and `comparator` are Lean programs. The pinned lean4export source
-uses Lean v4.33.0 by default, but its build command above deliberately selects
+uses Lean v4.34.0 by default, and its build command above deliberately selects
 the workspace's exact toolchain by copying `lean-toolchain`; different Lean
 releases have incompatible olean headers. Comparator builds `Challenge.olean` with the
 workspace toolchain and then reads it back with `lean4export`, so exact

diff --git a/SECURITY.md b/SECURITY.md
@@ -126,7 +126,7 @@ verifies on every run of the test suite that `lake env -- <cmd>` (and
 nested `lake env -- lake env -- <cmd>`) on a workspace whose
 `Submission.lean` has top-level `initialize` and `#eval` markers does
 NOT produce those markers in stdout. Confirmed on the pinned toolchain
-(Lean v4.33.0, 2026-08-14). If a future lake version starts evaluating project Lean
+(Lean v4.34.0, 2026-09-16). If a future lake version starts evaluating project Lean
 during `lake env`, this probe must be re-run before the toolchain
 bump lands.
 
@@ -212,12 +212,12 @@ time, the upstream publisher controls our supply chain.
 
 | Dependency | Repo | Pinned to | Purpose | Last bumped |
 |---|---|---|---|---|
-| Lean toolchain | leanprover/lean4 | `v4.33.0` | compiler and Lake | 2026-08-14 |
-| mathlib | leanprover-community/mathlib4 | `6f1ef4e5dd604a435bddba4747b13970cd65d2a1` | theorem library | 2026-08-14 |
-| lean4-cli | leanprover/lean4-cli | `6130a47896ce867c6a4a55373441e59e565bad0f` | command-line parsing | 2026-08-14 |
+| Lean toolchain | leanprover/lean4 | `v4.34.0` | compiler and Lake | 2026-09-16 |
+| mathlib | leanprover-community/mathlib4 | `5ed2965256430c3649e86755f9576b54eca72435` | theorem library | 2026-09-16 |
+| lean4-cli | leanprover/lean4-cli | `e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204` | command-line parsing | 2026-09-16 |
 | landrun | zouuup/landrun | `5ed4a3db3a4ad930d577215c6b9abaa19df7f99f` | Linux landlock sandbox | 2026-05-04 |
-| lean4export | leanprover/lean4export | `15f6055e299ad5b89345e533cc2192f4cc00f659` | exports olean to text | 2026-08-14 |
-| comparator | leanprover/comparator | `71b52ec29e06d4b7d882726553b1ceb99a2499e0` | the verifier | pre-2026-05 |
+| lean4export | leanprover/lean4export | `076e8e57707e813375e8f9da8bf989799ace9680` | exports olean to text | 2026-09-16 |
+| comparator | leanprover/comparator | `d03acab154d269c06e60e4de7e4cc85deebff94b` | the verifier | 2026-09-16 |
 | nanoda | robsimmons/nanoda_lib | `68d5ca9db226849b41a6fff59d796ff19d0a8840` | independent kernel (external checker) | 2026-07-29 |
 | `jlumbroso/free-disk-space` | (action) | `54081f138730dfa15788a46383842cd2f914a1be` | runner disk cleanup | 2026-05-04 |
 | `actions/checkout` | (action) | `3d3c42e5aac5ba805825da76410c181273ba90b1` (v7.0.1) | repo checkout | 2026-07-30 |

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -15,27 +15,27 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
+   "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "6130a47896ce867c6a4a55373441e59e565bad0f",
+   "inputRev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6f1ef4e5dd604a435bddba4747b13970cd65d2a1",
+   "rev": "5ed2965256430c3649e86755f9576b54eca72435",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "6f1ef4e5dd604a435bddba4747b13970cd65d2a1",
+   "inputRev": "5ed2965256430c3649e86755f9576b54eca72435",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb",
+   "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404",
+   "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "16f02aa7642864af59f1ff0e384a015994db9118",
+   "rev": "e928b72544873815af278d38681b31c0293588e3",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957",
+   "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e",
+   "rev": "355695d523e41d0554926416cba2a2b3544fbbc9",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81",
+   "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
+   "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

diff --git a/lakefile.toml b/lakefile.toml
@@ -7,12 +7,12 @@ autoImplicit = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "6f1ef4e5dd604a435bddba4747b13970cd65d2a1"
+rev = "5ed2965256430c3649e86755f9576b54eca72435"
 
 [[require]]
 name = "Cli"
 git = "https://github.com/leanprover/lean4-cli"
-rev = "6130a47896ce867c6a4a55373441e59e565bad0f"
+rev = "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204"
 
 [[require]]
 name = "lean-eval-generator"

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.33.0
+leanprover/lean4:v4.34.0