diff --git a/math/lean4/files/patch-stage0_src_runtime_object.cpp b/math/lean4/files/patch-stage0_src_runtime_object.cpp
new file mode 100644
index 000000000000..b6eca532c749
--- /dev/null
+++ b/math/lean4/files/patch-stage0_src_runtime_object.cpp
@@ -0,0 +1,15 @@
+-- workaround for https://github.com/leanprover/lean4/issues/14136
+-- Compilation fails: error: 'free_sized' is missing exception specification 'throw()'
+-- on FreeBSD 16
+
+--- stage0/src/runtime/object.cpp.orig	2026-06-22 01:22:24 UTC
++++ stage0/src/runtime/object.cpp
+@@ -61,7 +61,7 @@ __attribute__((nothrow))
+ // `__attribute__((nothrow))` to be present or `noexcept`.
+ __attribute__((nothrow))
+ #endif
+-__attribute__((weak)) void free_sized(void *ptr, size_t) {
++__attribute__((weak)) void free_sized(void *ptr, size_t) throw() {
+     free(ptr);
+ }
+ #endif