diff --git a/pkgs/build-support/lake/default.nix b/pkgs/build-support/lake/default.nix
index d2353fe0056a..f4baa5fae3cf 100644
--- a/pkgs/build-support/lake/default.nix
+++ b/pkgs/build-support/lake/default.nix
@@ -13,6 +13,7 @@
   gitMinimal,
   cacert,
   jq,
+  writableTmpDirAsHomeHook,
   writeText,
   stdenvNoCC,
 }:
@@ -113,48 +114,58 @@ lib.extendMkDerivation {
         lean4
         gitMinimal
         jq
+        writableTmpDirAsHomeHook
       ];
 
       propagatedBuildInputs = lib.optionals isLibrary leanDeps;
       buildInputs = lib.optionals (!isLibrary) leanDeps;
 
       configurePhase =
-        args.configurePhase or ''
-          runHook preConfigure
-
-          export HOME="$TMPDIR"
-
+        args.configurePhase or (
+          ''
+            runHook preConfigure
+          ''
           # Disable cloud caching and Reservoir lookups.
-          export LAKE_NO_CACHE=1
-          export RESERVOIR_API_URL=""
-          export LEAN_CC="${stdenv.cc}/bin/cc"
+          + ''
+            export LAKE_NO_CACHE=1
+            export RESERVOIR_API_URL=""
+            export LEAN_CC="${stdenv.cc}/bin/cc"
+          ''
+          # `lake` has no `-j`: it schedules build jobs on Lean's task manager, which otherwise
+          # sizes itself from `hardware_concurrency()` and ignores the builder's core budget.
+          + ''
+            export LEAN_NUM_THREADS="$NIX_BUILD_CORES"
 
-          if [ -n "''${LEAN_PATH:-}" ]; then
-            echo "buildLakePackage: LEAN_PATH=$LEAN_PATH"
-          fi
+            if [ -n "''${LEAN_PATH:-}" ]; then
+              echo "buildLakePackage: LEAN_PATH=$LEAN_PATH"
+            fi
 
-          ${lib.optionalString (computedLakeDeps != null) ''
-            mkdir -p .lake/packages
-            for dep in ${computedLakeDeps}/*; do
-              depName="$(basename "$dep")"
-              cp -r "$dep" ".lake/packages/$depName"
-              chmod -R u+w ".lake/packages/$depName"
-            done
+            ${lib.optionalString (computedLakeDeps != null) (
+              ''
+                mkdir -p .lake/packages
+                for dep in ${computedLakeDeps}/*; do
+                  depName="$(basename "$dep")"
+                  cp -r "$dep" ".lake/packages/$depName"
+                  chmod -R u+w ".lake/packages/$depName"
+                done
+              ''
+              # FOD deps use package-overrides.json (the on-disk mechanism).
+              # Nix-managed deps use --packages (the CLI mechanism, takes precedence).
+              + ''
+                jq -n --argjson pkgs "$(
+                  for dep in .lake/packages/*/; do
+                    [ -d "$dep" ] || continue
+                    depName="$(basename "$dep")"
+                    jq -n --arg name "$depName" --arg dir ".lake/packages/$depName" \
+                      '{type: "path", name: $name, inherited: false, dir: $dir}'
+                  done | jq -s '.'
+                )" '{schemaVersion: "1.2.0", packages: $pkgs}' > .lake/package-overrides.json
+              ''
+            )}
 
-            # FOD deps use package-overrides.json (the on-disk mechanism).
-            # Nix-managed deps use --packages (the CLI mechanism, takes precedence).
-            jq -n --argjson pkgs "$(
-              for dep in .lake/packages/*/; do
-                [ -d "$dep" ] || continue
-                depName="$(basename "$dep")"
-                jq -n --arg name "$depName" --arg dir ".lake/packages/$depName" \
-                  '{type: "path", name: $name, inherited: false, dir: $dir}'
-              done | jq -s '.'
-            )" '{schemaVersion: "1.2.0", packages: $pkgs}' > .lake/package-overrides.json
-          ''}
-
-          runHook postConfigure
-        '';
+            runHook postConfigure
+          ''
+        );
 
       buildPhase =
         args.buildPhase or ''
diff --git a/pkgs/by-name/le/lean4/mimalloc.patch b/pkgs/by-name/le/lean4/mimalloc.patch
deleted file mode 100644
index d69ae4eaae87..000000000000
--- a/pkgs/by-name/le/lean4/mimalloc.patch
+++ /dev/null
@@ -1,17 +0,0 @@
---- a/CMakeLists.txt
-+++ b/CMakeLists.txt
-@@ -80,11 +80,7 @@
-   ExternalProject_add(
-     mimalloc
-     PREFIX mimalloc
--    GIT_REPOSITORY https://github.com/microsoft/mimalloc
--    GIT_TAG v2.2.3
--    # just download, we compile it as part of each stage as it is small
--    CONFIGURE_COMMAND ""
--    BUILD_COMMAND ""
-+    SOURCE_DIR "MIMALLOC-SRC"
-     INSTALL_COMMAND ""
-   )
-   list(APPEND EXTRA_DEPENDS mimalloc)
- endif()
- 
diff --git a/pkgs/by-name/le/lean4/package.nix b/pkgs/by-name/le/lean4/package.nix
index 17913e8b1181..c179bade2728 100644
--- a/pkgs/by-name/le/lean4/package.nix
+++ b/pkgs/by-name/le/lean4/package.nix
@@ -4,38 +4,34 @@
   cmake,
   cctools,
   fetchFromGitHub,
-  git,
+  fetchpatch,
+  gitMinimal,
   gmp,
   cadical,
   leangz,
   makeWrapper,
+  openssl,
   pkg-config,
   libuv,
   enableMimalloc ? true,
   perl,
-  testers,
+  versionCheckHook,
 }:
 let
   cadical' = cadical.override { version = "2.1.3"; };
 in
 stdenv.mkDerivation (finalAttrs: {
   pname = "lean4";
-  version = "4.30.0";
+  version = "4.34.1";
 
-  # Using a vendored version rather than nixpkgs' version to match the exact version required by
-  # Lean.  Apparently, even a slight version change can impact greatly the final performance.
-  mimalloc-src = fetchFromGitHub {
-    owner = "microsoft";
-    repo = "mimalloc";
-    tag = "v2.2.3";
-    hash = "sha256-B0gngv16WFLBtrtG5NqA2m5e95bYVcQraeITcOX9A74=";
-  };
+  __structuredAttrs = true;
+  strictDeps = true;
 
   src = fetchFromGitHub {
     owner = "leanprover";
     repo = "lean4";
     tag = "v${finalAttrs.version}";
-    hash = "sha256-YTsfIppd6km7wOjAxRH5KMPsW++ztFDCJT2up72J86Q=";
+    hash = "sha256-JO1pCqWeotC4zjiIQZccEPXfVHnuDQC0DugyuJvIMRs=";
   };
 
   postPatch =
@@ -43,38 +39,38 @@ stdenv.mkDerivation (finalAttrs: {
       pattern = "\${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc";
     in
     ''
-      substituteInPlace src/CMakeLists.txt \
-        --replace-fail 'set(GIT_SHA1 "")' 'set(GIT_SHA1 "${finalAttrs.src.tag}")'
-
-      # Remove tests that fails in sandbox.
-      # It expects `sourceRoot` to be a git repository.
-      rm -rf src/lake/examples/git/
+      substituteInPlace \
+        src/CMakeLists.txt \
+        src/runtime/CMakeLists.txt \
+        stage0/src/CMakeLists.txt \
+        stage0/src/runtime/CMakeLists.txt \
+        --replace-fail '${pattern}' '${finalAttrs.mimalloc-src}'
     ''
-    + (lib.optionalString enableMimalloc ''
-      substituteInPlace CMakeLists.txt \
-        --replace-fail 'MIMALLOC-SRC' '${finalAttrs.mimalloc-src}'
-      for file in stage0/src/CMakeLists.txt stage0/src/runtime/CMakeLists.txt src/CMakeLists.txt src/runtime/CMakeLists.txt; do
-        substituteInPlace "$file" \
-          --replace-fail '${pattern}' '${finalAttrs.mimalloc-src}'
-      done
-    '');
+    # Remove tests that fails in sandbox.
+    # It expects `sourceRoot` to be a git repository.
+    + ''
+      rm -rf src/lake/examples/git/
+    '';
 
   preConfigure = ''
     patchShebangs stage0/src/bin/ src/bin/
   '';
 
   nativeBuildInputs = [
+    cadical'
     cmake
     pkg-config
     makeWrapper
     leangz # Provides leantar
   ]
-  ++ lib.optionals stdenv.hostPlatform.isDarwin [ cctools.libtool ];
+  ++ lib.optionals stdenv.hostPlatform.isDarwin [
+    cctools.libtool
+  ];
 
   buildInputs = [
     gmp
     libuv
-    cadical'
+    openssl
   ];
 
   postInstall = ''
@@ -83,26 +79,31 @@ stdenv.mkDerivation (finalAttrs: {
   '';
 
   nativeCheckInputs = [
-    git
+    gitMinimal
     perl
   ];
 
-  patches = [ ./mimalloc.patch ];
+  # Using a vendored version rather than nixpkgs' version to match the exact version required by
+  # Lean.  Apparently, even a slight version change can impact greatly the final performance.
+  mimalloc-src = fetchFromGitHub {
+    owner = "microsoft";
+    repo = "mimalloc";
+    tag = "v3.4.5";
+    hash = "sha256-vNVZw2YsDkf0GcdFTNb/fXMQLQYvoc8P425LupPShpo=";
+  };
 
   cmakeFlags = [
-    "-DUSE_GITHASH=OFF"
-    "-DINSTALL_LICENSE=OFF"
-    "-DINSTALL_CADICAL=OFF"
-    "-DSTAGE1_CMAKE_INSTALL_PREFIX=${placeholder "out"}"
-    "-DUSE_MIMALLOC=${if enableMimalloc then "ON" else "OFF"}"
+    (lib.cmakeBool "USE_GITHASH" false)
+    (lib.cmakeBool "INSTALL_LICENSE" false)
+    (lib.cmakeBool "INSTALL_CADICAL" false)
+    (lib.cmakeBool "USE_MIMALLOC" enableMimalloc)
+    (lib.cmakeFeature "FETCHCONTENT_SOURCE_DIR_MIMALLOC" finalAttrs.mimalloc-src.outPath)
   ];
 
-  passthru.tests = {
-    version = testers.testVersion {
-      package = finalAttrs.finalPackage;
-      version = "v${finalAttrs.version}";
-    };
-  };
+  nativeInstallCheckInputs = [
+    versionCheckHook
+  ];
+  doInstallCheck = true;
 
   meta = {
     description = "Automatic and interactive theorem prover";
diff --git a/pkgs/development/lean-modules/Cli/default.nix b/pkgs/development/lean-modules/Cli/default.nix
index d5bef89381c4..6d0a110ddfb3 100644
--- a/pkgs/development/lean-modules/Cli/default.nix
+++ b/pkgs/development/lean-modules/Cli/default.nix
@@ -7,13 +7,13 @@
 buildLakePackage (finalAttrs: {
   pname = "lean4-cli";
   # nixpkgs-update: no auto update
-  version = "4.30.0";
+  version = "4.34.0";
 
   src = fetchFromGitHub {
     owner = "leanprover";
     repo = "lean4-cli";
     tag = "v${finalAttrs.version}";
-    hash = "sha256-oMaqHvWlEfk1601JfNKPvkGIWgMW6tiF7Mej7g63vh0=";
+    hash = "sha256-3HLYlycvm4Ho98pB7eF+u8RN1GQJ7Ve6COqMSZr4Hic=";
   };
 
   leanPackageName = "Cli";
diff --git a/pkgs/development/lean-modules/LeanSearchClient/default.nix b/pkgs/development/lean-modules/LeanSearchClient/default.nix
index ad9267133806..3dd08914be38 100644
--- a/pkgs/development/lean-modules/LeanSearchClient/default.nix
+++ b/pkgs/development/lean-modules/LeanSearchClient/default.nix
@@ -7,13 +7,13 @@
 buildLakePackage {
   pname = "lean4-LeanSearchClient";
   # nixpkgs-update: no auto update
-  version = "4.12.0-unstable-2026-02-12";
+  version = "4.34.0-unstable-2026-09-14";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "LeanSearchClient";
-    rev = "c5d5b8fe6e5158def25cd28eb94e4141ad97c843";
-    hash = "sha256-L2aAwn3OeRLVt/VccLdBS0ogqmIIKAwnz94PpAOhaRc=";
+    rev = "ddf04cf3949fa556442341e87d47f9f6e6074707";
+    hash = "sha256-S2dp1E3Xv9b+U+r+b/MKGHviOg7ySE8QAX7EoB6Jbl8=";
   };
 
   leanPackageName = "LeanSearchClient";
diff --git a/pkgs/development/lean-modules/Qq/default.nix b/pkgs/development/lean-modules/Qq/default.nix
index dd89f7baa317..90693790e53a 100644
--- a/pkgs/development/lean-modules/Qq/default.nix
+++ b/pkgs/development/lean-modules/Qq/default.nix
@@ -7,13 +7,13 @@
 buildLakePackage {
   pname = "lean4-Qq";
   # nixpkgs-update: no auto update
-  version = "4.30.0";
+  version = "4.34.0-unstable-2026-09-14";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "quote4";
-    tag = "v4.30.0";
-    hash = "sha256-jVsRw/R7D7HmsE7vQvVeDXcnVerlcDBOrhf9FJJiXkY=";
+    rev = "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259";
+    hash = "sha256-fRsOiIgpS0YYWUsL/TwYn+orRC4rgNz7NSQ4+XCHCHQ=";
   };
 
   leanPackageName = "Qq";
diff --git a/pkgs/development/lean-modules/aesop/default.nix b/pkgs/development/lean-modules/aesop/default.nix
index f5c6393b3859..7c521ca27ace 100644
--- a/pkgs/development/lean-modules/aesop/default.nix
+++ b/pkgs/development/lean-modules/aesop/default.nix
@@ -8,13 +8,13 @@
 buildLakePackage {
   pname = "lean4-aesop";
   # nixpkgs-update: no auto update
-  version = "4.30.0";
+  version = "4.34.0-unstable-2026-09-14";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "aesop";
-    tag = "v4.30.0";
-    hash = "sha256-7PhQVMdiYImuzRYdf0Kgw3JYS4nBLfILXxyhFH8Zag0=";
+    rev = "355695d523e41d0554926416cba2a2b3544fbbc9";
+    hash = "sha256-yF2+P7H0B3546zopncnH2APEynRRJjTy+17OEAFovkE=";
   };
 
   leanPackageName = "aesop";
diff --git a/pkgs/development/lean-modules/batteries/default.nix b/pkgs/development/lean-modules/batteries/default.nix
index 5ac5ffadc806..ba1144ff869d 100644
--- a/pkgs/development/lean-modules/batteries/default.nix
+++ b/pkgs/development/lean-modules/batteries/default.nix
@@ -7,13 +7,13 @@
 buildLakePackage {
   pname = "lean4-batteries";
   # nixpkgs-update: no auto update
-  version = "4.30.0-unstable-2026-05-26";
+  version = "4.34.0-unstable-2026-09-14";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "batteries";
-    rev = "32dc18cde3684679f3c003de608743b57498c56f";
-    hash = "sha256-OOcKCQEgnn9zkkwjHOovMb/IprNomTDufLOfEXs7hFU=";
+    rev = "f2effa3d803fda822b1f97b806c47cf2adfbcbc2";
+    hash = "sha256-Y/Vfr3gVFfik2Rfshgu0iIn0IQYYCb6ShDt5nZe4RBc=";
   };
 
   leanPackageName = "batteries";
diff --git a/pkgs/development/lean-modules/importGraph/default.nix b/pkgs/development/lean-modules/importGraph/default.nix
index bda81c7ed521..54b6a560017b 100644
--- a/pkgs/development/lean-modules/importGraph/default.nix
+++ b/pkgs/development/lean-modules/importGraph/default.nix
@@ -8,13 +8,13 @@
 buildLakePackage {
   pname = "lean4-importGraph";
   # nixpkgs-update: no auto update
-  version = "4.30.0-unstable-2026-05-26";
+  version = "4.34.0-unstable-2026-09-14";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "import-graph";
-    rev = "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1";
-    hash = "sha256-V3bGQxTNs2G4MqaVxRb6WED1a7VaHfEo1HgBNqPipz8=";
+    rev = "e928b72544873815af278d38681b31c0293588e3";
+    hash = "sha256-U3eskYuk2vJ35IJqBsIgOHKL03UHtlEriyssNkBxwjM=";
   };
 
   leanPackageName = "importGraph";
diff --git a/pkgs/development/lean-modules/lean4/default.nix b/pkgs/development/lean-modules/lean4/default.nix
index d9ce64b4f591..68d507eb0803 100644
--- a/pkgs/development/lean-modules/lean4/default.nix
+++ b/pkgs/development/lean-modules/lean4/default.nix
@@ -6,11 +6,13 @@
   cmake,
   cctools,
   fetchFromGitHub,
+  fetchpatch,
   git,
   gmp,
   cadical,
   cadical' ? cadical.override { version = "2.1.3"; },
   leangz,
+  openssl,
   pkg-config,
   libuv,
   perl,
@@ -22,20 +24,20 @@
 let
   lean4 = stdenv.mkDerivation (finalAttrs: {
     pname = "lean4";
-    version = "4.30.0";
+    version = "4.34.1";
 
     mimalloc-src = fetchFromGitHub {
       owner = "microsoft";
       repo = "mimalloc";
-      tag = "v2.2.3";
-      hash = "sha256-B0gngv16WFLBtrtG5NqA2m5e95bYVcQraeITcOX9A74=";
+      tag = "v3.4.5";
+      hash = "sha256-vNVZw2YsDkf0GcdFTNb/fXMQLQYvoc8P425LupPShpo=";
     };
 
     src = fetchFromGitHub {
       owner = "leanprover";
       repo = "lean4";
       tag = "v${finalAttrs.version}";
-      hash = "sha256-YTsfIppd6km7wOjAxRH5KMPsW++ztFDCJT2up72J86Q=";
+      hash = "sha256-JO1pCqWeotC4zjiIQZccEPXfVHnuDQC0DugyuJvIMRs=";
     };
 
     # Vendor mimalloc. Upstream has since partially adopted FetchContent:
@@ -48,15 +50,6 @@ let
         pattern = "\${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc";
       in
       ''
-        substituteInPlace src/CMakeLists.txt \
-          --replace-fail 'set(GIT_SHA1 "")' 'set(GIT_SHA1 "${finalAttrs.src.tag}")'
-
-        rm -rf src/lake/examples/git/
-
-        substituteInPlace CMakeLists.txt \
-          --replace-fail 'GIT_REPOSITORY https://github.com/microsoft/mimalloc' \
-                         'SOURCE_DIR "${finalAttrs.mimalloc-src}"' \
-          --replace-fail 'GIT_TAG ${finalAttrs.mimalloc-src.tag}' ""
         for file in stage0/src/CMakeLists.txt stage0/src/runtime/CMakeLists.txt src/CMakeLists.txt src/runtime/CMakeLists.txt; do
           substituteInPlace "$file" \
             --replace-fail '${pattern}' '${finalAttrs.mimalloc-src}'
@@ -83,6 +76,7 @@ let
       gmp
       libuv
       cadical'
+      openssl
     ];
 
     nativeCheckInputs = [
@@ -95,8 +89,8 @@ let
       "-DINSTALL_LICENSE=OFF"
       "-DINSTALL_CADICAL=OFF"
       "-DINSTALL_LEANTAR=OFF"
-      "-DSTAGE1_CMAKE_INSTALL_PREFIX=${placeholder "out"}"
       "-DUSE_MIMALLOC=ON"
+      "-DFETCHCONTENT_SOURCE_DIR_MIMALLOC=${finalAttrs.mimalloc-src}"
     ];
 
     passthru.tests = {
diff --git a/pkgs/development/lean-modules/mathlib/default.nix b/pkgs/development/lean-modules/mathlib/default.nix
index eda7d235adba..0f839b07c61c 100644
--- a/pkgs/development/lean-modules/mathlib/default.nix
+++ b/pkgs/development/lean-modules/mathlib/default.nix
@@ -21,13 +21,13 @@ let
   mathlib__archive = buildLakePackage (finalAttrs: {
     pname = "lean4-mathlib";
     # nixpkgs-update: no auto update
-    version = "4.30.0";
+    version = "4.34.1";
 
     src = fetchFromGitHub {
       owner = "leanprover-community";
       repo = "mathlib4";
       tag = "v${finalAttrs.version}";
-      hash = "sha256-RxOxdUiVUAxUbfVhxlkjmPX1V64EtmIIn1eW75TiJWA=";
+      hash = "sha256-y3ql35O/z5fC9PSmMxqYAXZn63yByp3Z8LD00y9D2og=";
     };
 
     leanPackageName = "mathlib";
diff --git a/pkgs/development/lean-modules/plausible/default.nix b/pkgs/development/lean-modules/plausible/default.nix
index 34cf8fe6cb29..2163aae94fa7 100644
--- a/pkgs/development/lean-modules/plausible/default.nix
+++ b/pkgs/development/lean-modules/plausible/default.nix
@@ -7,13 +7,13 @@
 buildLakePackage {
   pname = "lean4-plausible";
   # nixpkgs-update: no auto update
-  version = "4.30.0-unstable-2026-05-26";
+  version = "4.34.0-unstable-2026-09-14";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "plausible";
-    rev = "a456461b368b71d2accd95234832cd9c174b5437";
-    hash = "sha256-DSaS0W2cfCUh2N+7WyiM7aUv3trtRNON0PzCgCW2SKY=";
+    rev = "118aa17ee84656b8bd727fef7c458ee8c833385c";
+    hash = "sha256-/ianaKsruF30J5tqK4vtbXsFd3mu4Xt8Ppj4ibHDEvg=";
   };
 
   leanPackageName = "plausible";
diff --git a/pkgs/development/lean-modules/proofwidgets/default.nix b/pkgs/development/lean-modules/proofwidgets/default.nix
index e0df936ad74c..850f26c5dcbe 100644
--- a/pkgs/development/lean-modules/proofwidgets/default.nix
+++ b/pkgs/development/lean-modules/proofwidgets/default.nix
@@ -10,13 +10,13 @@
 buildLakePackage (finalAttrs: {
   pname = "lean4-proofwidgets";
   # nixpkgs-update: no auto update
-  version = "0.0.99";
+  version = "0.0.111-unstable-2026-09-14";
 
   src = fetchFromGitHub {
     owner = "leanprover-community";
     repo = "ProofWidgets4";
-    tag = "v${finalAttrs.version}";
-    hash = "sha256-kGoEkKGrucNUWFYkHW2LsS1gI4C0J8bAHQL2MiE4Pzc=";
+    rev = "106ff4fafc74ef4ac99d81dbf3ab399118f497a5";
+    hash = "sha256-xjd3p+637F5q7xGTpDpy3/UCewpO8ArCfSAMAnAAjgs=";
   };
 
   leanPackageName = "proofwidgets";
@@ -32,7 +32,7 @@ buildLakePackage (finalAttrs: {
     name = "lean4-proofwidgets-npm-deps";
     src = finalAttrs.src;
     sourceRoot = "source/widget";
-    hash = "sha256-ssWSr2qfsIbX25DidiVPm0tsLGjrhQhQ6YKPL0rfc1k=";
+    hash = "sha256-z3LCBPmowLlkn5w/z72J1l8WnY60F8I7r48HMM/Lnns=";
   };
   npmRoot = "widget";