diff --git a/pkgs/development/lean-modules/mathlib/default.nix b/pkgs/development/lean-modules/mathlib/default.nix
index 6c70a6048613..adfce0b79ed6 100644
--- a/pkgs/development/lean-modules/mathlib/default.nix
+++ b/pkgs/development/lean-modules/mathlib/default.nix
@@ -1,6 +1,8 @@
 {
   lib,
   buildLakePackage,
+  runCommand,
+  xz,
   fetchFromGitHub,
   batteries,
   aesop,
@@ -12,43 +14,75 @@
   tests,
 }:
 
-buildLakePackage (finalAttrs: {
-  pname = "lean4-mathlib";
-  # nixpkgs-update: no auto update
-  version = "4.29.1";
+let
+  mathlib__archive = buildLakePackage (finalAttrs: {
+    pname = "lean4-mathlib";
+    # nixpkgs-update: no auto update
+    version = "4.29.1";
 
-  src = fetchFromGitHub {
-    owner = "leanprover-community";
-    repo = "mathlib4";
-    tag = "v${finalAttrs.version}";
-    hash = "sha256-K/QPTOytsV+OX25xyKlspeB9G0a28IjmJxcUAKXFP9U=";
-  };
+    src = fetchFromGitHub {
+      owner = "leanprover-community";
+      repo = "mathlib4";
+      tag = "v${finalAttrs.version}";
+      hash = "sha256-K/QPTOytsV+OX25xyKlspeB9G0a28IjmJxcUAKXFP9U=";
+    };
 
-  leanPackageName = "mathlib";
-  leanDeps = [
-    batteries
-    aesop
-    Qq
-    proofwidgets
-    plausible
-    LeanSearchClient
-    importGraph
-  ];
+    leanPackageName = "mathlib";
+    leanDeps = [
+      batteries
+      aesop
+      Qq
+      proofwidgets
+      plausible
+      LeanSearchClient
+      importGraph
+    ];
 
-  requiredSystemFeatures = [ "big-parallel" ];
+    nativeBuildInputs = [ xz ];
 
-  passthru.tests = {
-    inherit (tests.lake) weak-minimax;
-  };
+    # Compress the installed output into an xz archive so the derivation
+    # fits Hydra's max_output_size. The user-facing mathlib derivation
+    # decompresses transparently from this archive, at the de minimis
+    # compliance cost of nested compression.
+    postInstall = ''
+      tar cf - -C "$out" . | xz -T0 > "$TMPDIR/archive.tar.xz"
+      rm -rf "$out"
+      mkdir -p "$out"
+      mv "$TMPDIR/archive.tar.xz" "$out/"
+    '';
 
-  meta = {
-    description = "Mathematical library for Lean 4";
-    homepage = "https://github.com/leanprover-community/mathlib4";
-    license = lib.licenses.asl20;
-    # Output exceeds Hydra's 4 GiB NAR size limit. Oleans compress well with
-    # zstd (~70% ratio); a squashfs-packaged output would fit, pending upstream
-    # support or a raised limit.
-    hydraPlatforms = [ ];
-    maintainers = with lib.maintainers; [ nadja-y ];
-  };
-})
+    meta = {
+      description = "Mathematical library for Lean 4";
+      homepage = "https://github.com/leanprover-community/mathlib4";
+      license = lib.licenses.asl20;
+      maintainers = with lib.maintainers; [ nadja-y ];
+    };
+  });
+in
+
+runCommand mathlib__archive.name
+  {
+    nativeBuildInputs = [ xz ];
+    passthru = {
+      inherit mathlib__archive;
+      inherit (mathlib__archive)
+        src
+        version
+        lakePackageName
+        lean4
+        allLeanDeps
+        computedLakeDeps
+        overrideLakeDepsAttrs
+        ;
+      tests = {
+        inherit (tests.lake) weak-minimax;
+      };
+    };
+    meta = mathlib__archive.meta // {
+      hydraPlatforms = [ ];
+    };
+  }
+  ''
+    mkdir -p $out
+    xz -dT0 < ${mathlib__archive}/archive.tar.xz | tar xf - -C $out
+  ''
diff --git a/pkgs/top-level/lean-packages.nix b/pkgs/top-level/lean-packages.nix
index 7bdc715217cb..e52697bf149b 100644
--- a/pkgs/top-level/lean-packages.nix
+++ b/pkgs/top-level/lean-packages.nix
@@ -21,4 +21,5 @@ lib.makeScope newScope (self: {
   Cli = self.callPackage ../development/lean-modules/Cli { };
   importGraph = self.callPackage ../development/lean-modules/importGraph { };
   mathlib = self.callPackage ../development/lean-modules/mathlib { };
+  inherit (self.mathlib.passthru) mathlib__archive;
 })