diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp
index b9b964474463..4ba99d67bcbe 100644
--- a/src/library/constructions/projection.cpp
+++ b/src/library/constructions/projection.cpp
@@ -99,7 +99,10 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
         expr proj_val  = mk_proj(n, i, c);
         proj_val = lctx.mk_lambda(proj_args, proj_val);
         declaration new_d;
-        if (is_prop) {
+        // TODO: replace `if (false) {` with `if (is_prop) {`.
+        // Mathlib is crashing when prop fields are theorems.
+        // The crash is in the ir_interpreter. Kyle suspects this is an use-after-free bug in the interpreter.
+        if (false) { // if (is_prop) {
             bool unsafe = use_unsafe(env, proj_type) || use_unsafe(env, proj_val);
             if (unsafe) {
                 // theorems cannot be unsafe
diff --git a/tests/lean/run/2575.lean b/tests/lean/run/2575.lean
index c6d6f947c629..0ab4e8b299cb 100644
--- a/tests/lean/run/2575.lean
+++ b/tests/lean/run/2575.lean
@@ -4,8 +4,9 @@ structure AtLeastThirtySeven where
 
 theorem AtLeastThirtySeven.lt (x : AtLeastThirtySeven) : 36 < x.val := x.le
 
+-- TODO: fix
 /--
-info: theorem AtLeastThirtySeven.le : ∀ (self : AtLeastThirtySeven), 37 ≤ self.val :=
+info: def AtLeastThirtySeven.le : ∀ (self : AtLeastThirtySeven), 37 ≤ self.val :=
 fun self => self.2
 -/
 #guard_msgs in