diff --git a/math/lean4/files/patch-src_runtime_object.cpp b/math/lean4/files/patch-src_runtime_object.cpp
new file mode 100644
index 000000000000..c8a62465f1d7
--- /dev/null
+++ b/math/lean4/files/patch-src_runtime_object.cpp
@@ -0,0 +1,25 @@
+-- fix breakage caused by strict matching of the throw() attribute in FreeBSD 16.0
+
+--- src/runtime/object.cpp.orig	2026-06-21 11:16:11 UTC
++++ src/runtime/object.cpp
+@@ -22,6 +22,8 @@ Author: Leonardo de Moura
+ #include "runtime/io.h"
+ #include "runtime/hash.h"
+ 
++#include <sys/param.h>
++
+ #if defined(__GLIBC__) || defined(__APPLE__)
+     #define LEAN_SUPPORTS_BACKTRACE 1
+ #else
+@@ -61,7 +63,11 @@ __attribute__((nothrow))
+ // `__attribute__((nothrow))` to be present or `noexcept`.
+ __attribute__((nothrow))
+ #endif
++#if !defined(__FreeBSD__) || __FreeBSD_version < 1600000
+ __attribute__((weak)) void free_sized(void *ptr, size_t) {
++#else
++__attribute__((weak)) void free_sized(void *ptr, size_t) throw() {
++#endif
+     free(ptr);
+ }
+ #endif
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..ca40a370d5be
--- /dev/null
+++ b/math/lean4/files/patch-stage0_src_runtime_object.cpp
@@ -0,0 +1,25 @@
+-- fix breakage caused by strict matching of the throw() attribute in FreeBSD 16.0
+
+--- stage0/src/runtime/object.cpp.orig	2026-06-21 11:16:11 UTC
++++ stage0/src/runtime/object.cpp
+@@ -22,6 +22,8 @@ Author: Leonardo de Moura
+ #include "runtime/io.h"
+ #include "runtime/hash.h"
+ 
++#include <sys/param.h>
++
+ #if defined(__GLIBC__) || defined(__APPLE__)
+     #define LEAN_SUPPORTS_BACKTRACE 1
+ #else
+@@ -61,7 +63,11 @@ __attribute__((nothrow))
+ // `__attribute__((nothrow))` to be present or `noexcept`.
+ __attribute__((nothrow))
+ #endif
++#if !defined(__FreeBSD__) || __FreeBSD_version < 1600000
+ __attribute__((weak)) void free_sized(void *ptr, size_t) {
++#else
++__attribute__((weak)) void free_sized(void *ptr, size_t) throw() {
++#endif
+     free(ptr);
+ }
+ #endif