diff --git a/.envrc b/.envrc
new file mode 100644
index 0000000..3550a30
--- /dev/null
+++ b/.envrc
@@ -0,0 +1 @@
+use flake
diff --git a/.gitignore b/.gitignore
index 2a9fe5f..ecb70fd 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,4 @@
 /.lake
 /blake3
 result*
+.direnv/
diff --git a/flake.lock b/flake.lock
index 53038b9..9430540 100644
--- a/flake.lock
+++ b/flake.lock
@@ -59,11 +59,11 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1755389677,
-        "narHash": "sha256-q79j0+9Vr+QlRmJJijoXmEiMy2hl2lOXsLbjkGeAGnU=",
+        "lastModified": 1758037834,
+        "narHash": "sha256-P2rBelR9lgFJPE8kEV1wwX1LHK6xWlVcQqEez84ss6E=",
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "f6b97c79060dcbc7db0c2c9cde5061186c77f4af",
+        "rev": "d87ff09bad00ca4addd471a68a968f2aa29c7c36",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index 0f1c217..23929ed 100644
--- a/flake.nix
+++ b/flake.nix
@@ -60,7 +60,10 @@
           staticLib = lib.blake3-c;
         };
         devShells.default = pkgs.mkShell {
-          packages = with pkgs.lean; [lean lean-all pkgs.gcc pkgs.clang];
+          packages = with pkgs; [
+            lean.lean
+            lean.lean-all
+          ];
         };
 
         formatter = pkgs.alejandra;
diff --git a/lean-toolchain b/lean-toolchain
index 980709b..7f254a9 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.21.0
+leanprover/lean4:v4.23.0