diff --git a/build.rs b/build.rs
index 5c9234e..4355e4a 100644
--- a/build.rs
+++ b/build.rs
@@ -8,6 +8,7 @@ fn main() {
 	let input = format!("{lean_root}/include/lean/lean.h");
 	println!("cargo:rustc-link-search={callee_root}");
 	println!("cargo:rustc-link-search={lean_root}/lib/lean");
+	println!("cargo:rustc-link-lib=Init_shared");
 
 	let bindgen_dir = env::temp_dir().join("bindgen");
 	let extern_src_path = bindgen_dir.join("leanextern.c");
diff --git a/flake.lock b/flake.lock
index 26504e0..c36ba84 100644
--- a/flake.lock
+++ b/flake.lock
@@ -41,16 +41,16 @@
         "nixpkgs": "nixpkgs_2"
       },
       "locked": {
-        "lastModified": 1695693562,
-        "narHash": "sha256-6qbCafG0bL5KxQt2gL6hV4PFDsEMM0UXfldeOOqxsaE=",
+        "lastModified": 1709691092,
+        "narHash": "sha256-jHY8BhDotfGcMS0Xzl5iawqCaug3dDEKuD5Y1WcM06I=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "a832f398b80a5ebb820d27b9e55ec949759043ff",
+        "rev": "6fce8f7d5cd18a4419bca7fd51780c71c9b1cc5a",
         "type": "github"
       },
       "original": {
         "owner": "leanprover",
-        "ref": "v4.1.0",
+        "ref": "v4.7.0-rc2",
         "repo": "lean4",
         "type": "github"
       }
diff --git a/flake.nix b/flake.nix
index 2d2e05e..a05be36 100644
--- a/flake.nix
+++ b/flake.nix
@@ -4,7 +4,7 @@
   inputs = {
     nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean.url = "github:leanprover/lean4?ref=v4.1.0";
+    lean.url = "github:leanprover/lean4?ref=v4.7.0-rc2";
     rust-crate2nix = {
       url = "github:kolloch/crate2nix";
       flake = false;