diff --git a/c/raylib_bindings.c b/c/raylib_bindings.c
index ccff2ff..902a945 100644
--- a/c/raylib_bindings.c
+++ b/c/raylib_bindings.c
@@ -5,6 +5,15 @@
 #include <string.h>
 #include <stdlib.h>
 
+// Lean 4.30.0+ runs `main` on a new thread but UI should run on the OS main
+// thread (and this is mandatory on macOS), so opt out before `main` runs.
+// https://github.com/leanprover/lean4/pull/12971
+__attribute__((constructor))
+static void raylean_force_main_thread(void) {
+  // set overwrite=0 so users may force the threaded behavior using the shell
+  setenv("LEAN_MAIN_USE_THREAD", "0", 0);
+}
+
 #define IO_UNIT (lean_io_result_mk_ok(lean_box(0)))
 
 #ifdef RAYLEAN_NO_BUNDLE
diff --git a/lake-manifest.json b/lake-manifest.json
index 5a924c7..8121241 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,4 +1,4 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/funexists/lens-demo.git",
@@ -22,4 +22,5 @@
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "raylean",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/lean-toolchain b/lean-toolchain
index 4c685fa..af9e5d3 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.28.0
+leanprover/lean4:v4.30.0