diff --git a/flake.lock b/flake.lock
index dc83369..6bf8405 100644
--- a/flake.lock
+++ b/flake.lock
@@ -5,11 +5,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1709336216,
-        "narHash": "sha256-Dt/wOWeW6Sqm11Yh+2+t0dfEWxoMxGBvv3JpIocFl9E=",
+        "lastModified": 1727826117,
+        "narHash": "sha256-K5ZLCyfO/Zj9mPFldf3iwS6oZStJcU4tSpiXTMYaaL0=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "f7b3c975cf067e56e7cda6cb098ebe3fb4d74ca2",
+        "rev": "3d04084d54bedc3d6b8b736c70ef449225c361b1",
         "type": "github"
       },
       "original": {
@@ -18,40 +18,40 @@
         "type": "github"
       }
     },
-    "flake-utils": {
-      "locked": {
-        "lastModified": 1656928814,
-        "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
-        "owner": "numtide",
-        "repo": "flake-utils",
-        "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
-        "type": "github"
-      },
-      "original": {
-        "owner": "numtide",
-        "repo": "flake-utils",
-        "type": "github"
-      }
-    },
-    "lean": {
+    "flake-parts_2": {
       "inputs": {
-        "flake-utils": "flake-utils",
-        "nixpkgs": "nixpkgs",
-        "nixpkgs-cadical": "nixpkgs-cadical",
-        "nixpkgs-old": "nixpkgs-old"
+        "nixpkgs-lib": "nixpkgs-lib_2"
       },
       "locked": {
-        "lastModified": 1727749878,
-        "narHash": "sha256-O2Egyh2D0TfQWzQKfHUeAh7qAjMfeLVwXwGUw5QqcvE=",
-        "owner": "leanprover",
-        "repo": "lean4",
-        "rev": "dc2533473114eb8656439ff2b9335209784aa640",
+        "lastModified": 1727826117,
+        "narHash": "sha256-K5ZLCyfO/Zj9mPFldf3iwS6oZStJcU4tSpiXTMYaaL0=",
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "rev": "3d04084d54bedc3d6b8b736c70ef449225c361b1",
         "type": "github"
       },
       "original": {
-        "owner": "leanprover",
-        "ref": "v4.12.0",
-        "repo": "lean4",
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "type": "github"
+      }
+    },
+    "lean4-nix": {
+      "inputs": {
+        "flake-parts": "flake-parts_2",
+        "nixpkgs": "nixpkgs"
+      },
+      "locked": {
+        "lastModified": 1729990097,
+        "narHash": "sha256-3RUciZy/VMbyp9v1f8oba/oQ8bWWVh2+1wsuUah3ryE=",
+        "owner": "lenianiva",
+        "repo": "lean4-nix",
+        "rev": "6919763f186c7b0d39907203a649078ff3a4eb71",
+        "type": "github"
+      },
+      "original": {
+        "owner": "lenianiva",
+        "repo": "lean4-nix",
         "type": "github"
       }
     },
@@ -74,83 +74,56 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1686089707,
-        "narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
-        "owner": "NixOS",
+        "lastModified": 1728500571,
+        "narHash": "sha256-dOymOQ3AfNI4Z337yEwHGohrVQb4yPODCW9MDUyAc4w=",
+        "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
+        "rev": "d51c28603def282a24fa034bcb007e2bcb5b5dd0",
         "type": "github"
       },
       "original": {
-        "owner": "NixOS",
-        "ref": "nixpkgs-unstable",
+        "owner": "nixos",
+        "ref": "nixos-24.05",
         "repo": "nixpkgs",
         "type": "github"
       }
     },
-    "nixpkgs-cadical": {
-      "locked": {
-        "lastModified": 1722221733,
-        "narHash": "sha256-sga9SrrPb+pQJxG1ttJfMPheZvDOxApFfwXCFO0H9xw=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "12bf09802d77264e441f48e25459c10c93eada2e",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "12bf09802d77264e441f48e25459c10c93eada2e",
-        "type": "github"
-      }
-    },
     "nixpkgs-lib": {
       "locked": {
-        "dir": "lib",
-        "lastModified": 1709237383,
-        "narHash": "sha256-cy6ArO4k5qTx+l5o+0mL9f5fa86tYUX3ozE1S+Txlds=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "1536926ef5621b09bba54035ae2bb6d806d72ac8",
-        "type": "github"
+        "lastModified": 1727825735,
+        "narHash": "sha256-0xHYkMkeLVQAMa7gvkddbPqpxph+hDzdu1XdGPJR+Os=",
+        "type": "tarball",
+        "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
       },
       "original": {
-        "dir": "lib",
-        "owner": "NixOS",
-        "ref": "nixos-unstable",
-        "repo": "nixpkgs",
-        "type": "github"
+        "type": "tarball",
+        "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
       }
     },
-    "nixpkgs-old": {
-      "flake": false,
+    "nixpkgs-lib_2": {
       "locked": {
-        "lastModified": 1581379743,
-        "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
-        "type": "github"
+        "lastModified": 1727825735,
+        "narHash": "sha256-0xHYkMkeLVQAMa7gvkddbPqpxph+hDzdu1XdGPJR+Os=",
+        "type": "tarball",
+        "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
       },
       "original": {
-        "owner": "NixOS",
-        "ref": "nixos-19.03",
-        "repo": "nixpkgs",
-        "type": "github"
+        "type": "tarball",
+        "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
       }
     },
     "nixpkgs_2": {
       "locked": {
-        "lastModified": 1711703276,
-        "narHash": "sha256-iMUFArF0WCatKK6RzfUJknjem0H9m4KgorO/p3Dopkk=",
+        "lastModified": 1729691686,
+        "narHash": "sha256-BAuPWW+9fa1moZTU+jFh+1cUtmsuF8asgzFwejM4wac=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "d8fe5e6c92d0d190646fb9f1056741a229980089",
+        "rev": "32e940c7c420600ef0d1ef396dc63b04ee9cad37",
         "type": "github"
       },
       "original": {
         "owner": "nixos",
-        "ref": "nixos-unstable",
+        "ref": "nixos-24.05",
         "repo": "nixpkgs",
         "type": "github"
       }
@@ -158,7 +131,7 @@
     "root": {
       "inputs": {
         "flake-parts": "flake-parts",
-        "lean": "lean",
+        "lean4-nix": "lean4-nix",
         "lspec": "lspec",
         "nixpkgs": "nixpkgs_2"
       }
diff --git a/flake.nix b/flake.nix
index d4c903f..2c1a76e 100644
--- a/flake.nix
+++ b/flake.nix
@@ -2,12 +2,9 @@
   description = "Pantograph";
 
   inputs = {
-    nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
+    nixpkgs.url = "github:nixos/nixpkgs/nixos-24.05";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean = {
-      # Do not follow input's nixpkgs since it could cause build failures
-      url = "github:leanprover/lean4?ref=v4.12.0";
-    };
+    lean4-nix.url = "github:lenianiva/lean4-nix";
     lspec = {
       url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab";
       flake = false;
@@ -18,7 +15,7 @@
     self,
     nixpkgs,
     flake-parts,
-    lean,
+    lean4-nix,
     lspec,
     ...
   } : flake-parts.lib.mkFlake { inherit inputs; } {
@@ -29,13 +26,16 @@
       "x86_64-darwin"
     ];
     perSystem = { system, pkgs, ... }: let
-      leanPkgs = lean.packages.${system}.deprecated;
-      lspecLib = leanPkgs.buildLeanPackage {
+      pkgs = import nixpkgs {
+        inherit system;
+        overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ];
+      };
+      lspecLib = pkgs.lean.buildLeanPackage {
         name = "LSpec";
         roots = [ "Main" "LSpec" ];
         src = "${lspec}";
       };
-      project = leanPkgs.buildLeanPackage {
+      project = pkgs.lean.buildLeanPackage {
         name = "Pantograph";
         roots = [ "Pantograph" ];
         src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
@@ -46,7 +46,7 @@
             !(pkgs.lib.hasSuffix "Repl.lean" path);
         });
       };
-      repl = leanPkgs.buildLeanPackage {
+      repl = pkgs.lean.buildLeanPackage {
         name = "Repl";
         roots = [ "Main" "Repl" ];
         deps = [ project ];
@@ -57,7 +57,7 @@
             !(pkgs.lib.hasSuffix ".md" path);
         });
       };
-      test = leanPkgs.buildLeanPackage {
+      test = pkgs.lean.buildLeanPackage {
         name = "Test";
         # NOTE: The src directory must be ./. since that is where the import
         # root begins (e.g. `import Test.Environment` and not `import
@@ -72,24 +72,25 @@
       };
     in rec {
       packages = {
-        inherit (leanPkgs) lean lean-all;
+        inherit (pkgs.lean) lean lean-all;
         inherit (project) sharedLib;
         inherit (repl) executable;
         default = repl.executable;
       };
       legacyPackages = {
-        inherit project leanPkgs;
+        inherit project;
+        leanPkgs = pkgs.lean;
       };
       checks = {
         test = pkgs.runCommand "test" {
-          buildInputs = [ test.executable leanPkgs.lean-all ];
+          buildInputs = [ test.executable pkgs.lean.lean-all ];
         } ''
           #export LEAN_SRC_PATH="${./.}"
           ${test.executable}/bin/test > $out
         '';
       };
       devShells.default = pkgs.mkShell {
-        buildInputs = [ leanPkgs.lean-all leanPkgs.lean ];
+        buildInputs = [ pkgs.lean.lean-all pkgs.lean.lean ];
       };
     };
   };