diff --git a/src/lake/.envrc b/src/lake/.envrc
deleted file mode 100644
index 3550a30f2d..0000000000
--- a/src/lake/.envrc
+++ /dev/null
@@ -1 +0,0 @@
-use flake
diff --git a/src/lake/README.md b/src/lake/README.md
index 140ccf6fbb..7c24646588 100644
--- a/src/lake/README.md
+++ b/src/lake/README.md
@@ -360,15 +360,7 @@ After building, the `lake` binary will be located at `build/bin/lake` and the li
 
 ### Building with Nix Flakes
 
-It is also possible to build Lake with the Nix setup `buildLeanPackage` from the [`lean4`](https://github.com/leanprover/lean4) repository. To do so, you need to have Nix installed with flakes enabled. It is recommended to also set up the Lean 4 binary cache as described in the Lean 4 repository.
-
-It is then possible to build Lake with `nix build .` or run it from anywhere with `nix run github:leanprover/lake`.
-
-A development environment with Lean 4 installed can be loaded automatically by running `nix develop` or automatically on `cd` with `direnv` by running `direnv allow`.
-
-The versions of `nixpkgs` and `lean4` are fixed to specific hashes. They can be updated by running `nix flake update`.
-
-Thank Anders Christiansen Sørby ([@Anderssorby](https://github.com/Anderssorby)) for this support!
+Lake is built as part of the main Lean 4 flake at the repository root.
 
 ### Augmenting Lake's Search Path
 
diff --git a/src/lake/flake.nix b/src/lake/flake.nix
deleted file mode 100644
index 26f685158d..0000000000
--- a/src/lake/flake.nix
+++ /dev/null
@@ -1,56 +0,0 @@
-{
-  description = "Lake (Lean Make) is a new build system and package manager for Lean 4.";
-
-  inputs = {
-    nixpkgs.url = "github:nixos/nixpkgs/nixos-21.05";
-    lean = {
-      url = "github:leanprover/lean4";
-    };
-    flake-utils = {
-      url = "github:numtide/flake-utils";
-      inputs.nixpkgs.follows = "nixpkgs";
-    };
-  };
-
-  outputs =
-    { self
-    , flake-utils
-    , nixpkgs
-    , lean
-    }:
-    flake-utils.lib.eachDefaultSystem (system:
-    let
-      pkgs = import nixpkgs { inherit system; };
-      packageName = "Lake";
-      src = ./.;
-      leanPkgs = lean.packages.${system};
-      project = leanPkgs.buildLeanPackage {
-        name = packageName;
-        inherit src;
-      };
-      cli = leanPkgs.buildLeanPackage {
-        name = "Lake.Main";
-        executableName = "lake";
-        deps = [ project ];
-        linkFlags = pkgs.lib.optional pkgs.stdenv.isLinux "-rdynamic";
-        inherit src;
-      };
-    in
-    {
-      packages = project // {
-        inherit (leanPkgs) lean;
-
-        cli = cli.executable;
-      };
-
-      defaultPackage = self.packages.${system}.cli;
-
-      apps.lake = flake-utils.lib.mkApp {
-        drv = cli.executable;
-      };
-
-      defaultApp = self.apps.${system}.lake;
-
-      inherit (project) devShell;
-    });
-}