diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean
index 506583021b..bc320bda42 100644
--- a/src/Init/Grind/Tactics.lean
+++ b/src/Init/Grind/Tactics.lean
@@ -120,6 +120,10 @@ structure Config where
   the characteristic of a ring.
   -/
   exp : Nat := 2^20
+  /--
+  When `true` (default: `true`), automatically creates an auxiliary theorem to store the proof.
+  -/
+  abstractProof := true
   deriving Inhabited, BEq
 
 end Lean.Grind
diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean
index f0d153a2d0..b3a27732c0 100644
--- a/src/Lean/Elab/Tactic/Grind.lean
+++ b/src/Lean/Elab/Tactic/Grind.lean
@@ -161,8 +161,10 @@ def grind
     if result.hasFailed then
       throwError "`grind` failed\n{← result.toMessageData}"
     trace[grind.debug.proof] "{← instantiateMVars mvar'}"
-    -- `grind` proofs are often big
-    let e ← if (← isProp type) then
+    -- `grind` proofs are often big, if `abstractProof` is true, we create an auxiliary theorem.
+    let e ← if !config.abstractProof then
+      instantiateMVarsProfiling mvar'
+    else if (← isProp type) then
       mkAuxTheorem type (← instantiateMVarsProfiling mvar') (zetaDelta := true)
     else
       let auxName ← Term.mkAuxName `grind