diff --git a/maintainers/maintainer-list.nix b/maintainers/maintainer-list.nix
index e27a2181dc90..49a4cbcb7956 100644
--- a/maintainers/maintainer-list.nix
+++ b/maintainers/maintainer-list.nix
@@ -18701,6 +18701,12 @@
     githubId = 23151917;
     name = "nadir-ishiguro";
   };
+  nadja-y = {
+    email = "git@njy.dev";
+    github = "nadja-y";
+    githubId = 255079535;
+    name = "Nadja Yang";
+  };
   nadrieril = {
     email = "nadrieril@gmail.com";
     github = "Nadrieril";
diff --git a/pkgs/build-support/lake/default.nix b/pkgs/build-support/lake/default.nix
new file mode 100644
index 000000000000..42344a7797ff
--- /dev/null
+++ b/pkgs/build-support/lake/default.nix
@@ -0,0 +1,326 @@
+# buildLakePackage: build Lean 4 projects that use the Lake build system.
+#
+# Dependencies can be provided in two ways:
+#   - `leanDeps`: already-packaged Lean libraries from leanPackages.
+#     These are injected into LEAN_PATH via setup hooks and propagated
+#     transitively, similar to Haskell's libraryHaskellDepends.
+#   - `lakeHash`: SRI hash for a fetchLakeDeps FOD that clones git
+#     dependencies listed in lake-manifest.json (like buildGoModule's
+#     vendorHash).  Not needed when all deps are in `leanDeps`.
+#
+# Library output layout:
+#   $out/                         Package root (source + build artifacts)
+#   $out/lakefile.{lean,toml}     Lake package configuration
+#   $out/lean-toolchain           Lean version pin
+#   $out/.lake/build/lib/lean/    Compiled .olean/.ilean files
+#   $out/.lake/build/ir/          Compiled C/object files
+#   $out/nix-support/setup-hook   LEAN_PATH propagation hook
+{
+  lib,
+  stdenv,
+  lean4,
+  gitMinimal,
+  cacert,
+  jq,
+  lndir,
+  stdenvNoCC,
+}:
+
+let
+  fetchLakeDeps = import ./fetch-lake-deps.nix {
+    inherit
+      lib
+      stdenvNoCC
+      gitMinimal
+      cacert
+      jq
+      ;
+  };
+in
+
+lib.extendMkDerivation {
+  constructDrv = stdenv.mkDerivation;
+  excludeDrvArgNames = [
+    "lakeHash"
+    "lakeDeps"
+    "leanDeps"
+    "buildTargets"
+    "isLibrary"
+    "leanPackageName"
+    "overrideLakeDepsAttrs"
+  ];
+  extendDrvArgs =
+    finalAttrs:
+    {
+      nativeBuildInputs ? [ ],
+      passthru ? { },
+
+      # SRI hash for the Lake dependencies FOD.
+      # Set to null if the project has no external dependencies
+      # (or all deps are provided via leanDeps).
+      lakeHash ? null,
+
+      # Pre-built Lake dependencies derivation (overrides lakeHash).
+      lakeDeps ? null,
+
+      # Already-packaged Lean libraries from nixpkgs.
+      # These are added to LEAN_PATH (via setup hook) and propagated
+      # transitively.  Each must be a buildLakePackage output with
+      # .olean files under $out/.lake/build/lib/lean/.
+      leanDeps ? [ ],
+
+      # Lean package name as declared in lakefile.lean/toml.
+      # Defaults to pname.
+      leanPackageName ? finalAttrs.pname,
+
+      # Lake build targets.  Empty list means the default target.
+      buildTargets ? [ ],
+
+      # Whether this is a library (install full package tree with
+      # .olean/.ilean files) or an executable (install binaries only).
+      isLibrary ? true,
+
+      # Override attributes of the lakeDeps derivation.
+      overrideLakeDepsAttrs ? (finalAttrs: previousAttrs: { }),
+
+      meta ? { },
+
+      ...
+    }@args:
+    let
+      lakeDeps' = args.lakeDeps or null;
+      lakeHash = args.lakeHash or null;
+      leanDeps = args.leanDeps or [ ];
+      overrideLakeDepsAttrs = args.overrideLakeDepsAttrs or (_: _: { });
+      buildTargets = args.buildTargets or [ ];
+      isLibrary = args.isLibrary or true;
+      leanPackageName = args.leanPackageName or finalAttrs.pname;
+
+      computedLakeDeps =
+        if lakeDeps' != null then
+          lakeDeps'
+        else if lakeHash == null then
+          null
+        else
+          (fetchLakeDeps {
+            name = finalAttrs.name or "${finalAttrs.pname}-${finalAttrs.version}";
+            inherit (finalAttrs) src;
+            hash = lakeHash;
+            sourceRoot = finalAttrs.sourceRoot or "";
+            patches = finalAttrs.patches or [ ];
+            prePatch = finalAttrs.prePatch or "";
+            postPatch = finalAttrs.postPatch or "";
+            excludePackages = builtins.map (dep: dep.passthru.lakePackageName or dep.pname) allLeanDeps;
+          }).overrideAttrs
+            (lib.toExtension overrideLakeDepsAttrs);
+
+      # Transitively collect all Lean dependencies.  Each buildLakePackage
+      # library stores its own transitive closure in passthru.allLeanDeps,
+      # so this flattens the entire dependency DAG.
+      allLeanDeps = lib.unique (
+        builtins.concatMap (dep: [ dep ] ++ (dep.passthru.allLeanDeps or [ ])) leanDeps
+      );
+    in
+    {
+      strictDeps = true;
+
+      nativeBuildInputs = nativeBuildInputs ++ [
+        lean4
+        gitMinimal
+        jq
+        lndir
+      ];
+
+      # Propagate so downstream packages get transitive LEAN_PATH entries
+      # via each dependency's nix-support/setup-hook.
+      propagatedBuildInputs = lib.optionals isLibrary leanDeps;
+
+      # Executables only need deps at build time.
+      buildInputs = lib.optionals (!isLibrary) leanDeps;
+
+      configurePhase =
+        args.configurePhase or ''
+          runHook preConfigure
+
+          export HOME="$TMPDIR"
+
+          # Disable Lake cloud caching and Reservoir lookups
+          export LAKE_NO_CACHE=1
+          export RESERVOIR_API_URL=""
+
+          # Point leanc at the nix-provided C compiler
+          export LEAN_CC="${stdenv.cc}/bin/cc"
+
+          # Validate that the lean-toolchain file (if present) matches the
+          # Lean toolchain we are building against.  Mismatches between the
+          # toolchain version and the compiler produce confusing errors, so
+          # fail early with a clear message.
+          leanVersion="${lean4.version}"
+          if [ -f lean-toolchain ]; then
+            toolchainVersion=$(sed -n 's/^.*:v\([0-9][0-9.]*\).*/\1/p' lean-toolchain)
+            if [ -n "$toolchainVersion" ] && [ "$toolchainVersion" != "$leanVersion" ]; then
+              echo "buildLakePackage: lean-toolchain requests v$toolchainVersion but lean4 is v$leanVersion" >&2
+              echo "buildLakePackage: update the package or use a matching lean4 version" >&2
+              exit 1
+            fi
+          fi
+
+          ${lib.concatStringsSep "\n" (
+            builtins.map (
+              dep:
+              let
+                name = dep.passthru.lakePackageName or dep.pname;
+              in
+              ''
+                # Fail fast if nix-packaged dep "${name}" was built against a
+                # different Lean version.  This avoids wasting build time when
+                # the package set is mid-update (e.g. lean4 bumped but a dep
+                # has not been updated yet).
+                if [ -f "${dep}/lean-toolchain" ]; then
+                  depToolchain=$(sed -n 's/^.*:v\([0-9][0-9.]*\).*/\1/p' "${dep}/lean-toolchain")
+                  if [ -n "$depToolchain" ] && [ "$depToolchain" != "$leanVersion" ]; then
+                    echo "buildLakePackage: dependency ${name} was built with Lean v$depToolchain but lean4 is v$leanVersion" >&2
+                    echo "buildLakePackage: update ${name} first, or override lean4 in leanPackages" >&2
+                    exit 1
+                  fi
+                fi
+              ''
+            ) allLeanDeps
+          )}
+
+          if [ -n "''${LEAN_PATH:-}" ]; then
+            echo "buildLakePackage: LEAN_PATH=$LEAN_PATH"
+          fi
+
+          mkdir -p .lake/packages
+
+          # Create a minimal empty manifest if none exists.  Lake requires
+          # this file, but when all deps come from leanDeps (nix-managed),
+          # the actual dependency entries come from package-overrides.json.
+          if [ ! -f lake-manifest.json ]; then
+            echo '{"version":"1.1.0","packagesDir":".lake/packages","packages":[]}' \
+              > lake-manifest.json
+          fi
+
+          ${lib.optionalString (computedLakeDeps != null) ''
+            # Copy fetched (not yet nix-packaged) deps into .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.concatStringsSep "\n" (
+            builtins.map (
+              dep:
+              let
+                name = dep.passthru.lakePackageName or dep.pname;
+              in
+              ''
+                # Install nix-packaged dep "${name}" into .lake/packages/.
+                # lndir creates a symlink tree so artifacts remain as
+                # zero-copy references to the store; writable dirs let Lake
+                # create metadata during workspace initialization.
+                rm -rf ".lake/packages/${name}"
+                mkdir -p ".lake/packages/${name}"
+                lndir -silent "${dep}" ".lake/packages/${name}"
+              ''
+            ) allLeanDeps
+          )}
+
+          # Generate package-overrides.json redirecting deps to local
+          # paths.  Scans .lake/packages/ so that nix-managed deps work
+          # even without a lake-manifest.json (like Haskell's package DB
+          # approach — nix is the sole dependency provider, Lake just
+          # validates against lakefile.lean at build time).
+          if [ -d .lake/packages ] && [ -n "$(ls -A .lake/packages/ 2>/dev/null)" ]; then
+            jq -n --argjson pkgs "$(
+              for dep in .lake/packages/*/; do
+                [ -d "$dep" ] || continue
+                depName="$(basename "$dep")"
+                printf '{"type":"path","name":"%s","inherited":false,"configFile":"lakefile","dir":".lake/packages/%s"}\n' \
+                  "$depName" "$depName"
+              done | jq -s '.'
+            )" '{schemaVersion: "1.1.0", packages: $pkgs}' > .lake/package-overrides.json
+          fi
+
+          runHook postConfigure
+        '';
+
+      buildPhase =
+        args.buildPhase or ''
+          runHook preBuild
+
+          local targets="${lib.concatStringsSep " " buildTargets}"
+          echo "buildLakePackage: building ''${targets:-default targets}"
+
+          lake build --no-ansi $targets
+
+          runHook postBuild
+        '';
+
+      installPhase =
+        args.installPhase or (
+          if isLibrary then
+            ''
+              runHook preInstall
+
+              # Install the complete Lake package tree.  $out/ IS the
+              # package directory — source, lakefile, and pre-built
+              # artifacts under .lake/build/.
+              cp -rT . "$out"
+
+              # Remove build-environment artifacts that reference the
+              # build sandbox or dependency store paths.
+              rm -rf "$out/.lake/packages"
+              rm -f "$out/.lake/package-overrides.json"
+
+              # Install the setup hook so that downstream derivations
+              # (and `nix develop` shells) automatically get this
+              # package's oleans in LEAN_PATH.
+              mkdir -p "$out/nix-support"
+              cp ${./setup-hook.sh} "$out/nix-support/setup-hook"
+
+              # Symlink any built executables into $out/bin/ for
+              # discoverability (e.g. packages that are both libraries
+              # and executables).
+              if [ -d "$out/.lake/build/bin" ]; then
+                mkdir -p "$out/bin"
+                for exe in "$out/.lake/build/bin"/*; do
+                  if [ -f "$exe" ] && [ -x "$exe" ]; then
+                    ln -s "../.lake/build/bin/$(basename "$exe")" "$out/bin/$(basename "$exe")"
+                  fi
+                done
+              fi
+
+              runHook postInstall
+            ''
+          else
+            ''
+              runHook preInstall
+
+              # Install executables only.
+              if [ -d .lake/build/bin ]; then
+                mkdir -p "$out/bin"
+                find .lake/build/bin -type f -executable \
+                  -exec install -Dm755 {} "$out/bin/" \;
+              fi
+
+              runHook postInstall
+            ''
+        );
+
+      passthru = passthru // {
+        inherit computedLakeDeps lean4 allLeanDeps;
+        lakePackageName = leanPackageName;
+        # Canonicalize overrideLakeDepsAttrs as an attribute overlay,
+        # following the same pattern as buildGoModule's overrideModAttrs.
+        overrideLakeDepsAttrs = lib.toExtension overrideLakeDepsAttrs;
+      };
+
+      meta = meta // {
+        platforms = meta.platforms or lean4.meta.platforms;
+      };
+    };
+}
diff --git a/pkgs/build-support/lake/fetch-lake-deps.nix b/pkgs/build-support/lake/fetch-lake-deps.nix
new file mode 100644
index 000000000000..acd165b8d7cd
--- /dev/null
+++ b/pkgs/build-support/lake/fetch-lake-deps.nix
@@ -0,0 +1,95 @@
+# fetchLakeDeps: fixed-output derivation that fetches Lake dependencies.
+#
+# Reads lake-manifest.json from the source tree, clones each git
+# dependency at its pinned revision, and produces a directory of
+# package sources.  The output is hash-verified via `lakeHash`.
+#
+# This follows the same pattern as buildGoModule's `goModules` FOD.
+{
+  lib,
+  stdenvNoCC,
+  gitMinimal,
+  cacert,
+  jq,
+}:
+
+{
+  name,
+  src,
+  hash,
+  sourceRoot ? "",
+  patches ? [ ],
+  prePatch ? "",
+  postPatch ? "",
+  # Package names to skip (e.g. already packaged in nix).
+  excludePackages ? [ ],
+}:
+
+stdenvNoCC.mkDerivation {
+  name = "${name}-lake-deps";
+
+  inherit
+    src
+    sourceRoot
+    patches
+    prePatch
+    postPatch
+    ;
+
+  nativeBuildInputs = [
+    gitMinimal
+    cacert
+    jq
+  ];
+
+  impureEnvVars = lib.fetchers.proxyImpureEnvVars ++ [
+    "GIT_PROXY_COMMAND"
+    "SOCKS_SERVER"
+  ];
+
+  dontConfigure = true;
+
+  buildPhase = ''
+    runHook preBuild
+
+    if [ ! -f lake-manifest.json ]; then
+      echo "fetchLakeDeps: lake-manifest.json not found" >&2
+      exit 1
+    fi
+
+    export HOME="$TMPDIR"
+    export GIT_SSL_CAINFO="$NIX_SSL_CERT_FILE"
+
+    mkdir -p "$TMPDIR/packages"
+
+    jq -c --argjson exclude ${lib.escapeShellArg (builtins.toJSON excludePackages)} \
+      '.packages[] | select(.type == "git") | select(.name as $n | $exclude | index($n) | not)' \
+      lake-manifest.json | while IFS= read -r pkg; do
+      name=$(echo "$pkg" | jq -r '.name')
+      url=$(echo "$pkg" | jq -r '.url')
+      rev=$(echo "$pkg" | jq -r '.rev')
+
+      echo "fetchLakeDeps: cloning $name ($url @ $rev)"
+
+      git clone --filter=blob:none --no-checkout "$url" "$TMPDIR/packages/$name"
+      git -C "$TMPDIR/packages/$name" checkout "$rev" --quiet
+
+      # Remove .git to make output deterministic
+      rm -rf "$TMPDIR/packages/$name/.git"
+    done
+
+    runHook postBuild
+  '';
+
+  installPhase = ''
+    runHook preInstall
+    mv "$TMPDIR/packages" "$out"
+    runHook postInstall
+  '';
+
+  dontFixup = true;
+
+  outputHashMode = "recursive";
+  outputHash = hash;
+  outputHashAlgo = if hash == "" then "sha256" else null;
+}
diff --git a/pkgs/build-support/lake/setup-hook.sh b/pkgs/build-support/lake/setup-hook.sh
new file mode 100644
index 000000000000..0c7cd93dd90f
--- /dev/null
+++ b/pkgs/build-support/lake/setup-hook.sh
@@ -0,0 +1,8 @@
+addLeanPath() {
+    local buildLib="$1/.lake/build/lib/lean"
+    if [ -d "$buildLib" ]; then
+        addToSearchPath LEAN_PATH "$buildLib"
+    fi
+}
+
+addEnvHooks "$hostOffset" addLeanPath
diff --git a/pkgs/build-support/lake/test/default.nix b/pkgs/build-support/lake/test/default.nix
new file mode 100644
index 000000000000..b31cb5f70d5c
--- /dev/null
+++ b/pkgs/build-support/lake/test/default.nix
@@ -0,0 +1,8 @@
+{
+  lib,
+  callPackage,
+}:
+
+lib.recurseIntoAttrs {
+  weak-minimax = callPackage ./weak-minimax/package.nix { };
+}
diff --git a/pkgs/build-support/lake/test/weak-minimax/Main.lean b/pkgs/build-support/lake/test/weak-minimax/Main.lean
new file mode 100644
index 000000000000..490b95b07e82
--- /dev/null
+++ b/pkgs/build-support/lake/test/weak-minimax/Main.lean
@@ -0,0 +1,4 @@
+import WeakMinimax
+
+def main : IO Unit := do
+  IO.println "weak_minimax: verified (maximin <= minimax)"
diff --git a/pkgs/build-support/lake/test/weak-minimax/WeakMinimax.lean b/pkgs/build-support/lake/test/weak-minimax/WeakMinimax.lean
new file mode 100644
index 000000000000..2930f68e93eb
--- /dev/null
+++ b/pkgs/build-support/lake/test/weak-minimax/WeakMinimax.lean
@@ -0,0 +1,9 @@
+import Mathlib.Order.CompleteLattice.Basic
+
+/-- Weak minimax inequality (weak duality): maximin ≤ minimax.
+For any payoff f into a complete lattice, the best worst-case guarantee
+for the maximizing player never exceeds the minimax value. -/
+theorem weak_minimax {ι κ α : Type*} [CompleteLattice α]
+    (f : ι → κ → α) :
+    ⨆ i, ⨅ j, f i j ≤ ⨅ j, ⨆ i, f i j :=
+  iSup_iInf_le_iInf_iSup f
diff --git a/pkgs/build-support/lake/test/weak-minimax/lakefile.lean b/pkgs/build-support/lake/test/weak-minimax/lakefile.lean
new file mode 100644
index 000000000000..9937799396d1
--- /dev/null
+++ b/pkgs/build-support/lake/test/weak-minimax/lakefile.lean
@@ -0,0 +1,12 @@
+import Lake
+open Lake DSL
+
+package weakMinimax
+
+require "leanprover-community" / "mathlib" @ git "main"
+
+@[default_target] lean_lib WeakMinimax
+
+@[default_target]
+lean_exe weakMinimax.run where
+  root := `Main
diff --git a/pkgs/build-support/lake/test/weak-minimax/package.nix b/pkgs/build-support/lake/test/weak-minimax/package.nix
new file mode 100644
index 000000000000..5e6114486792
--- /dev/null
+++ b/pkgs/build-support/lake/test/weak-minimax/package.nix
@@ -0,0 +1,40 @@
+# Test that buildLakePackage works with nix-only deps (no lake-manifest.json).
+# Builds a Lean proof of the weak minimax inequality using mathlib.
+#
+# Note: building the executable recompiles .c → .c.o for all transitive
+# dependency modules because library packages only ship .olean/.ilean/.c
+# artifacts (the default Lake library facet).  Lake's trace system would
+# reuse pre-built object files if present, but since Lean 4 is rarely
+# used for application code, we defer shipping .o files in library
+# packages to keep store footprint minimal.
+{
+  leanPackages,
+  runCommand,
+}:
+
+let
+  inherit (leanPackages) buildLakePackage mathlib;
+
+  testPackage = buildLakePackage {
+    pname = "weak-minimax";
+    version = "0";
+    src = ./.;
+
+    leanDeps = [ mathlib ];
+  };
+in
+
+runCommand "buildLakePackage-weak-minimax"
+  {
+    nativeBuildInputs = [ testPackage ];
+  }
+  ''
+    mkdir -p $out
+
+    # Verify the executable runs (proof was verified at build time).
+    weakMinimax-run | tee $out/result
+    grep -q "weak_minimax" $out/result
+
+    # Verify library output has compiled oleans.
+    test -d "${testPackage}/.lake/build/lib/lean"
+  ''
diff --git a/pkgs/by-name/le/lean4/package.nix b/pkgs/by-name/le/lean4/package.nix
index fbe9891ea4ed..7f7c8962b0ba 100644
--- a/pkgs/by-name/le/lean4/package.nix
+++ b/pkgs/by-name/le/lean4/package.nix
@@ -98,6 +98,7 @@ stdenv.mkDerivation (finalAttrs: {
     maintainers = with lib.maintainers; [
       danielbritten
       jthulhu
+      nadja-y
     ];
     mainProgram = "lean";
   };
diff --git a/pkgs/development/lean-modules/Cli/default.nix b/pkgs/development/lean-modules/Cli/default.nix
new file mode 100644
index 000000000000..0177c09973db
--- /dev/null
+++ b/pkgs/development/lean-modules/Cli/default.nix
@@ -0,0 +1,26 @@
+{
+  lib,
+  buildLakePackage,
+  fetchFromGitHub,
+}:
+
+buildLakePackage {
+  pname = "lean4-cli";
+  version = "4.28.0";
+
+  src = fetchFromGitHub {
+    owner = "leanprover";
+    repo = "lean4-cli";
+    tag = "v4.28.0";
+    hash = "sha256-9nX+dozmDAaVb5uKWL14zbILr7aqbVerTyPcN12Niw4=";
+  };
+
+  leanPackageName = "Cli";
+
+  meta = {
+    description = "Command-line argument parser for Lean 4";
+    homepage = "https://github.com/leanprover/lean4-cli";
+    license = lib.licenses.mit;
+    maintainers = with lib.maintainers; [ nadja-y ];
+  };
+}
diff --git a/pkgs/development/lean-modules/LeanSearchClient/default.nix b/pkgs/development/lean-modules/LeanSearchClient/default.nix
new file mode 100644
index 000000000000..bce5fe166814
--- /dev/null
+++ b/pkgs/development/lean-modules/LeanSearchClient/default.nix
@@ -0,0 +1,33 @@
+{
+  lib,
+  buildLakePackage,
+  fetchFromGitHub,
+}:
+
+buildLakePackage {
+  pname = "lean4-LeanSearchClient";
+  # No lockstep tags; version pinned by mathlib's lake-manifest.json.
+  version = "0-unstable-2026-02-12";
+
+  src = fetchFromGitHub {
+    owner = "leanprover-community";
+    repo = "LeanSearchClient";
+    rev = "c5d5b8fe6e5158def25cd28eb94e4141ad97c843";
+    hash = "sha256-L2aAwn3OeRLVt/VccLdBS0ogqmIIKAwnz94PpAOhaRc=";
+  };
+
+  leanPackageName = "LeanSearchClient";
+
+  # Upstream lean-toolchain lags behind; remove it so the
+  # buildLakePackage toolchain check does not reject this package.
+  postPatch = ''
+    rm -f lean-toolchain
+  '';
+
+  meta = {
+    description = "Lean 4 client for LeanSearch and Moogle proof search";
+    homepage = "https://github.com/leanprover-community/LeanSearchClient";
+    license = lib.licenses.asl20;
+    maintainers = with lib.maintainers; [ nadja-y ];
+  };
+}
diff --git a/pkgs/development/lean-modules/Qq/default.nix b/pkgs/development/lean-modules/Qq/default.nix
new file mode 100644
index 000000000000..6939b121939c
--- /dev/null
+++ b/pkgs/development/lean-modules/Qq/default.nix
@@ -0,0 +1,26 @@
+{
+  lib,
+  buildLakePackage,
+  fetchFromGitHub,
+}:
+
+buildLakePackage {
+  pname = "lean4-Qq";
+  version = "4.28.0";
+
+  src = fetchFromGitHub {
+    owner = "leanprover-community";
+    repo = "quote4";
+    tag = "v4.28.0";
+    hash = "sha256-BRrSdDJQAsgM/NeSL2FODCez/8zEffjDRWUToGlKDNQ=";
+  };
+
+  leanPackageName = "Qq";
+
+  meta = {
+    description = "Lean 4 compile-time quote and antiquote macros for metaprogramming";
+    homepage = "https://github.com/leanprover-community/quote4";
+    license = lib.licenses.asl20;
+    maintainers = with lib.maintainers; [ nadja-y ];
+  };
+}
diff --git a/pkgs/development/lean-modules/aesop/default.nix b/pkgs/development/lean-modules/aesop/default.nix
new file mode 100644
index 000000000000..e60651dbe2a0
--- /dev/null
+++ b/pkgs/development/lean-modules/aesop/default.nix
@@ -0,0 +1,28 @@
+{
+  lib,
+  buildLakePackage,
+  fetchFromGitHub,
+  batteries,
+}:
+
+buildLakePackage {
+  pname = "lean4-aesop";
+  version = "4.28.0";
+
+  src = fetchFromGitHub {
+    owner = "leanprover-community";
+    repo = "aesop";
+    tag = "v4.28.0";
+    hash = "sha256-KeP46qtEf4/lgi4iCVuYIQbazufTR4luTbsuia9JkK4=";
+  };
+
+  leanPackageName = "aesop";
+  leanDeps = [ batteries ];
+
+  meta = {
+    description = "White-box automation for Lean 4";
+    homepage = "https://github.com/leanprover-community/aesop";
+    license = lib.licenses.asl20;
+    maintainers = with lib.maintainers; [ nadja-y ];
+  };
+}
diff --git a/pkgs/development/lean-modules/batteries/default.nix b/pkgs/development/lean-modules/batteries/default.nix
new file mode 100644
index 000000000000..af0b8623e1c6
--- /dev/null
+++ b/pkgs/development/lean-modules/batteries/default.nix
@@ -0,0 +1,26 @@
+{
+  lib,
+  buildLakePackage,
+  fetchFromGitHub,
+}:
+
+buildLakePackage {
+  pname = "lean4-batteries";
+  version = "4.28.0";
+
+  src = fetchFromGitHub {
+    owner = "leanprover-community";
+    repo = "batteries";
+    tag = "v4.28.0";
+    hash = "sha256-3N1MCFsg5UiwBCMAhDK7WwIowMNnhjlFgAsm0UPtGKc=";
+  };
+
+  leanPackageName = "batteries";
+
+  meta = {
+    description = "The batteries-included extended library for Lean 4";
+    homepage = "https://github.com/leanprover-community/batteries";
+    license = lib.licenses.asl20;
+    maintainers = with lib.maintainers; [ nadja-y ];
+  };
+}
diff --git a/pkgs/development/lean-modules/importGraph/default.nix b/pkgs/development/lean-modules/importGraph/default.nix
new file mode 100644
index 000000000000..50a91b3c819f
--- /dev/null
+++ b/pkgs/development/lean-modules/importGraph/default.nix
@@ -0,0 +1,28 @@
+{
+  lib,
+  buildLakePackage,
+  fetchFromGitHub,
+  Cli,
+}:
+
+buildLakePackage {
+  pname = "lean4-importGraph";
+  version = "4.28.0";
+
+  src = fetchFromGitHub {
+    owner = "leanprover-community";
+    repo = "import-graph";
+    tag = "v4.28.0";
+    hash = "sha256-fZS8bFQjV7eLZCJwD+SVRzmCcCthrl+PO8vL8U8AOYs=";
+  };
+
+  leanPackageName = "importGraph";
+  leanDeps = [ Cli ];
+
+  meta = {
+    description = "Tools to analyse and visualise Lean 4 import structures";
+    homepage = "https://github.com/leanprover-community/import-graph";
+    license = lib.licenses.asl20;
+    maintainers = with lib.maintainers; [ nadja-y ];
+  };
+}
diff --git a/pkgs/development/lean-modules/mathlib/default.nix b/pkgs/development/lean-modules/mathlib/default.nix
new file mode 100644
index 000000000000..77d935a79a44
--- /dev/null
+++ b/pkgs/development/lean-modules/mathlib/default.nix
@@ -0,0 +1,47 @@
+{
+  lib,
+  buildLakePackage,
+  fetchFromGitHub,
+  batteries,
+  aesop,
+  Qq,
+  proofwidgets,
+  plausible,
+  LeanSearchClient,
+  importGraph,
+  tests,
+}:
+
+buildLakePackage {
+  pname = "lean4-mathlib";
+  version = "4.28.0";
+
+  src = fetchFromGitHub {
+    owner = "leanprover-community";
+    repo = "mathlib4";
+    tag = "v4.28.0";
+    hash = "sha256-7kR0WvEDey5kEdqKKVEO/JgQd1VyB6a+zwPvIV5E5Pg=";
+  };
+
+  leanPackageName = "mathlib";
+  leanDeps = [
+    batteries
+    aesop
+    Qq
+    proofwidgets
+    plausible
+    LeanSearchClient
+    importGraph
+  ];
+
+  passthru.tests = {
+    inherit (tests.lake) weak-minimax;
+  };
+
+  meta = {
+    description = "Mathematical library for Lean 4";
+    homepage = "https://github.com/leanprover-community/mathlib4";
+    license = lib.licenses.asl20;
+    maintainers = with lib.maintainers; [ nadja-y ];
+  };
+}
diff --git a/pkgs/development/lean-modules/plausible/default.nix b/pkgs/development/lean-modules/plausible/default.nix
new file mode 100644
index 000000000000..dc61bca2c751
--- /dev/null
+++ b/pkgs/development/lean-modules/plausible/default.nix
@@ -0,0 +1,26 @@
+{
+  lib,
+  buildLakePackage,
+  fetchFromGitHub,
+}:
+
+buildLakePackage {
+  pname = "lean4-plausible";
+  version = "4.28.0";
+
+  src = fetchFromGitHub {
+    owner = "leanprover-community";
+    repo = "plausible";
+    tag = "v4.28.0";
+    hash = "sha256-xuOfeoRPt5L0Rk4fEJPIi1A0aoNIkC1fsh5yeIx5bFI=";
+  };
+
+  leanPackageName = "plausible";
+
+  meta = {
+    description = "Property-based testing framework for Lean 4";
+    homepage = "https://github.com/leanprover-community/plausible";
+    license = lib.licenses.asl20;
+    maintainers = with lib.maintainers; [ nadja-y ];
+  };
+}
diff --git a/pkgs/development/lean-modules/proofwidgets/default.nix b/pkgs/development/lean-modules/proofwidgets/default.nix
new file mode 100644
index 000000000000..c026f0c62bcc
--- /dev/null
+++ b/pkgs/development/lean-modules/proofwidgets/default.nix
@@ -0,0 +1,68 @@
+{
+  lib,
+  buildLakePackage,
+  fetchFromGitHub,
+  fetchNpmDeps,
+  npmHooks,
+  nodejs,
+}:
+
+let
+  src = fetchFromGitHub {
+    owner = "leanprover-community";
+    repo = "ProofWidgets4";
+    tag = "v0.0.87";
+    hash = "sha256-qXEqNfwUBPnxAtLRkBZTBFhrM4JYl43gLo/PM6HOG7o=";
+  };
+in
+
+buildLakePackage {
+  pname = "lean4-proofwidgets";
+  version = "0.0.87";
+
+  inherit src;
+
+  leanPackageName = "proofwidgets";
+
+  # ProofWidgets has no Lean dependencies (lake-manifest.json packages = []).
+  lakeHash = null;
+
+  nativeBuildInputs = [
+    nodejs
+    npmHooks.npmConfigHook
+  ];
+
+  # Pre-fetched npm dependencies for the TypeScript widget build
+  # (npm/rollup in widget/).  npmConfigHook installs these offline.
+  npmDeps = fetchNpmDeps {
+    name = "lean4-proofwidgets-npm-deps";
+    inherit src;
+    sourceRoot = "source/widget";
+    hash = "sha256-CzBRrreOSytquZ/xFHPlY8r+lz5Bg9Zk9ienRhc8SiY=";
+  };
+  npmRoot = "widget";
+
+  # Lake's widgetJsAll target runs `npm clean-install` which wipes
+  # node_modules and the patched shebangs that npmConfigHook applied.
+  # Wrap npm to skip ci/clean-install (deps already installed) while
+  # passing `npm run build` through — same pattern as llama-cpp/evcc.
+  postConfigure = ''
+    local realNpm
+    realNpm="$(type -P npm)"
+    mkdir -p "$TMPDIR/npm-wrap"
+    cat > "$TMPDIR/npm-wrap/npm" <<WRAPPER
+    #!/bin/sh
+    case "\$1" in ci|clean-install) exit 0 ;; esac
+    exec "$realNpm" "\$@"
+    WRAPPER
+    chmod +x "$TMPDIR/npm-wrap/npm"
+    export PATH="$TMPDIR/npm-wrap:$PATH"
+  '';
+
+  meta = {
+    description = "Interactive UI framework for Lean 4 proof assistants";
+    homepage = "https://github.com/leanprover-community/ProofWidgets4";
+    license = lib.licenses.asl20;
+    maintainers = with lib.maintainers; [ nadja-y ];
+  };
+}
diff --git a/pkgs/development/lean-modules/update.sh b/pkgs/development/lean-modules/update.sh
new file mode 100755
index 000000000000..a02e52d6775f
--- /dev/null
+++ b/pkgs/development/lean-modules/update.sh
@@ -0,0 +1,83 @@
+#!/usr/bin/env nix-shell
+#!nix-shell -i bash -p nix-update common-updater-scripts curl jq
+
+# Update all leanPackages to match the lean4 version in nixpkgs.
+#
+# All mathlib-ecosystem packages (batteries, aesop, Qq, plausible,
+# importGraph, Cli, mathlib) release with the same version tag as
+# lean4 (lockstep versioning).  ProofWidgets and LeanSearchClient
+# have their own versioning; the correct versions are read from
+# mathlib's lake-manifest.json at the matching lean4 tag.
+#
+# This script only prefetches source hashes — it does not build
+# anything.  Output is a summary suitable for commit messages.
+#
+# Usage:
+#   ./pkgs/development/lean-modules/update.sh
+
+set -euo pipefail
+
+lean4_version=$(nix eval --raw .#lean4.version)
+
+# Snapshot current versions for diffing.
+old_lockstep=$(nix eval --raw .#leanPackages.mathlib.version 2>/dev/null || echo "")
+old_pw=$(nix eval --raw .#leanPackages.proofwidgets.version 2>/dev/null || echo "")
+old_lsc=$(nix eval --raw .#leanPackages.LeanSearchClient.version 2>/dev/null || echo "")
+
+manifest=$(curl -sL "https://raw.githubusercontent.com/leanprover-community/mathlib4/v${lean4_version}/lake-manifest.json")
+
+# Verify that mathlib's dependency set matches what we package.
+# If mathlib adds or removes a dep, this script needs manual updating.
+known_deps="Cli LeanSearchClient Qq aesop batteries importGraph plausible proofwidgets"
+manifest_deps=$(echo "$manifest" | jq -r '[.packages[].name] | sort | join(" ")')
+if [ "$manifest_deps" != "$known_deps" ]; then
+  echo "ERROR: mathlib dependency set has changed" >&2
+  echo "  expected: $known_deps" >&2
+  echo "  got:      $manifest_deps" >&2
+  exit 1
+fi
+
+pw_version=$(echo "$manifest" | jq -r '.packages[] | select(.name == "proofwidgets") | .inputRev' | sed 's/^v//')
+
+lsc_rev=$(echo "$manifest" | jq -r '.packages[] | select(.name == "LeanSearchClient") | .rev')
+lsc_date=$(curl -sL "https://api.github.com/repos/leanprover-community/LeanSearchClient/commits/$lsc_rev" | jq -r '.commit.committer.date[:10]')
+lsc_version="0-unstable-$lsc_date"
+
+# Leaf packages (no leanDeps).
+nix-update leanPackages.batteries        --version="$lean4_version"
+nix-update leanPackages.Qq               --version="$lean4_version"
+nix-update leanPackages.plausible        --version="$lean4_version"
+nix-update leanPackages.Cli              --version="$lean4_version"
+nix-update leanPackages.proofwidgets     --version="$pw_version"
+
+# LeanSearchClient has no lockstep tags; pin to the exact rev mathlib uses.
+update-source-version leanPackages.LeanSearchClient "$lsc_version" \
+  --rev="$lsc_rev"
+
+# Packages with leanDeps.
+nix-update leanPackages.aesop            --version="$lean4_version"
+nix-update leanPackages.importGraph      --version="$lean4_version"
+
+# mathlib (all deps are nix-packaged, no lakeHash needed).
+nix-update leanPackages.mathlib          --version="$lean4_version"
+
+# Summary.
+changes=()
+if [ "$old_lockstep" != "$lean4_version" ]; then
+  changes+=("lockstep packages: $old_lockstep -> $lean4_version")
+fi
+if [ "$old_pw" != "$pw_version" ]; then
+  changes+=("proofwidgets: $old_pw -> $pw_version")
+fi
+if [ "$old_lsc" != "$lsc_version" ]; then
+  changes+=("LeanSearchClient: $old_lsc -> $lsc_version")
+fi
+
+if [ ${#changes[@]} -eq 0 ]; then
+  echo "leanPackages: already up to date at lean4 $lean4_version"
+else
+  echo "leanPackages: update to lean4 $lean4_version"
+  for c in "${changes[@]}"; do
+    echo "  - $c"
+  done
+fi
diff --git a/pkgs/test/default.nix b/pkgs/test/default.nix
index acd0982ed5f8..27bd1bb34d04 100644
--- a/pkgs/test/default.nix
+++ b/pkgs/test/default.nix
@@ -172,6 +172,8 @@ in
 
   go = recurseIntoAttrs (callPackage ../build-support/go/tests.nix { });
 
+  lake = callPackage ../build-support/lake/test { };
+
   pkg-config = recurseIntoAttrs (callPackage ../top-level/pkg-config/tests.nix { });
 
   buildRustCrate = recurseIntoAttrs (callPackage ../build-support/rust/build-rust-crate/test { });
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 3336049b8904..75de0d300208 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -307,6 +307,8 @@ with pkgs;
   buildFHSEnvChroot = callPackage ../build-support/build-fhsenv-chroot { }; # Deprecated; use buildFHSEnv/buildFHSEnvBubblewrap
   buildFHSEnvBubblewrap = callPackage ../build-support/build-fhsenv-bubblewrap { };
 
+  buildLakePackage = callPackage ../build-support/lake { };
+
   cameractrls-gtk4 = cameractrls.override { withGtk = 4; };
 
   cameractrls-gtk3 = cameractrls.override { withGtk = 3; };
@@ -2845,6 +2847,8 @@ with pkgs;
 
   leanblueprint = with python3Packages; toPythonApplication leanblueprint;
 
+  leanPackages = callPackage ../top-level/lean-packages.nix { };
+
   inherit (callPackage ../development/tools/lerna { })
     lerna_6
     lerna_8
diff --git a/pkgs/top-level/lean-packages.nix b/pkgs/top-level/lean-packages.nix
new file mode 100644
index 000000000000..64314343a910
--- /dev/null
+++ b/pkgs/top-level/lean-packages.nix
@@ -0,0 +1,45 @@
+# Lean 4 package set.
+#
+# All packages are built against a single Lean toolchain version.
+# Dependencies between packages use `leanDeps` which propagates
+# .olean files via LEAN_PATH (through setup hooks), similar to how
+# Haskell propagates package.conf.d entries.
+#
+# Overriding lean4 propagates to all packages in the set:
+#   leanPackages.overrideScope (self: super: { lean4 = lean4-custom; })
+#
+# Usage:
+#   leanPackages.batteries
+#   leanPackages.mathlib
+#   leanPackages.callPackage ./my-package.nix { }
+{
+  lib,
+  newScope,
+  lean4,
+}:
+
+lib.makeScope newScope (self: {
+  inherit lean4;
+
+  # Resolve via self.callPackage so overriding lean4 in the scope
+  # propagates to the builder (same pattern as coqPackages).
+  buildLakePackage = self.callPackage ../build-support/lake { };
+
+  batteries = self.callPackage ../development/lean-modules/batteries { };
+
+  aesop = self.callPackage ../development/lean-modules/aesop { };
+
+  Qq = self.callPackage ../development/lean-modules/Qq { };
+
+  proofwidgets = self.callPackage ../development/lean-modules/proofwidgets { };
+
+  plausible = self.callPackage ../development/lean-modules/plausible { };
+
+  LeanSearchClient = self.callPackage ../development/lean-modules/LeanSearchClient { };
+
+  Cli = self.callPackage ../development/lean-modules/Cli { };
+
+  importGraph = self.callPackage ../development/lean-modules/importGraph { };
+
+  mathlib = self.callPackage ../development/lean-modules/mathlib { };
+})