diff --git a/mathlib4/lakefile.lean b/mathlib4/lakefile.lean
index 1c2f6bf57..4d799a378 100644
--- a/mathlib4/lakefile.lean
+++ b/mathlib4/lakefile.lean
@@ -44,6 +44,7 @@ abbrev mathlibLeanOptions := #[
     ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
     ⟨`autoImplicit, false⟩,
     ⟨`maxSynthPendingDepth, .ofNat 3⟩,
+    ⟨`debug.skipKernelTC, true⟩,
   ] ++ -- options that are used in `lake build`
     mathlibOnlyLinters.map fun s ↦ { s with name := `weak ++ s.name }