diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
index 8a0e614c85c4..5064dbb28e0f 100644
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h
@@ -1011,13 +1011,13 @@ static inline lean_object * lean_array_get_size(b_lean_obj_arg a) {
     return lean_box(lean_array_size(a));
 }
 
-static inline lean_object * lean_mk_empty_array() {
-    return lean_alloc_array(0, 0);
-}
+LEAN_EXPORT lean_object * lean_mk_empty_array(void);
 
 static inline lean_object * lean_mk_empty_array_with_capacity(b_lean_obj_arg capacity) {
     if (!lean_is_scalar(capacity)) lean_internal_panic_out_of_memory();
-    return lean_alloc_array(0, lean_unbox(capacity));
+    size_t c = lean_unbox(capacity);
+    if (c == 0) return lean_mk_empty_array();
+    return lean_alloc_array(0, c);
 }
 
 static inline lean_object * lean_array_uget(b_lean_obj_arg a, size_t i) {
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index 9954c2c5d77d..8becddeede31 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -495,6 +495,10 @@ static obj_res mk_closure_3_2(lean_cfun3 fn, obj_arg a1, obj_arg a2) {
 static object * g_array_empty = nullptr;
 
 object * array_mk_empty() {
+    return lean_mk_empty_array();
+}
+
+extern "C" LEAN_EXPORT object * lean_mk_empty_array() {
     return g_array_empty;
 }
 
diff --git a/tests/compile/array_empty_cached.lean b/tests/compile/array_empty_cached.lean
new file mode 100644
index 000000000000..d97147d774c5
--- /dev/null
+++ b/tests/compile/array_empty_cached.lean
@@ -0,0 +1,29 @@
+module
+
+import Init.Data.Array.Basic
+import Init.Util
+
+/-!
+Tests that zero-capacity arrays reuse the runtime's cached empty array.
+-/
+
+set_option compiler.extract_closed false
+
+@[noinline] def empty : Unit → Array Nat := fun _ => Array.empty
+
+@[noinline] def emptyLiteral : Unit → Array Nat := fun _ => #[]
+
+@[noinline] def emptyWithCapacity : Unit → Array Nat := fun _ => Array.emptyWithCapacity 0
+
+@[noinline] def mkEmpty : Unit → Array Nat := fun _ => Array.mkEmpty 0
+
+@[noinline] def emptyWithPositiveCapacity : Unit → Array Nat := fun _ => Array.emptyWithCapacity 1
+
+public unsafe def main : IO Unit := do
+  let xs := empty ()
+  IO.println (ptrEq xs (emptyLiteral ()))
+  IO.println (ptrEq xs (emptyWithCapacity ()))
+  IO.println (ptrEq xs (mkEmpty ()))
+  IO.println (isExclusiveUnsafe (emptyWithPositiveCapacity ()))
+  let ys := xs.push 42
+  IO.println (xs.isEmpty && ys == #[42])
diff --git a/tests/compile/array_empty_cached.lean.no_interpret b/tests/compile/array_empty_cached.lean.no_interpret
new file mode 100644
index 000000000000..b40d70a0f080
--- /dev/null
+++ b/tests/compile/array_empty_cached.lean.no_interpret
@@ -0,0 +1 @@
+The interpreter does not model native reference-count exclusivity.
diff --git a/tests/compile/array_empty_cached.lean.out.expected b/tests/compile/array_empty_cached.lean.out.expected
new file mode 100644
index 000000000000..36c7afad66a1
--- /dev/null
+++ b/tests/compile/array_empty_cached.lean.out.expected
@@ -0,0 +1,5 @@
+true
+true
+true
+true
+true