diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean
index 8e7bed47e4..f748cbf685 100644
--- a/src/Lean/Data/Name.lean
+++ b/src/Lean/Data/Name.lean
@@ -132,6 +132,7 @@ def isInternalDetail : Name → Bool
       || matchPrefix s "eq_"
       || matchPrefix s "match_"
       || matchPrefix s "proof_"
+      || matchPrefix s "omega_"
       || p.isInternalOrNum
   | .num _ _     => true
   | p            => p.isInternalOrNum
diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean
index ce08b338ab..1eb742eec1 100644
--- a/src/Lean/Elab/Tactic/Omega/Frontend.lean
+++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean
@@ -7,6 +7,8 @@ prelude
 import Lean.Elab.Tactic.Omega.Core
 import Lean.Elab.Tactic.FalseOrByContra
 import Lean.Elab.Tactic.Config
+import Lean.Elab.MutualDef
+import Lean.Meta.Closure
 
 /-!
 # Frontend to the `omega` tactic.
@@ -670,12 +672,19 @@ open Lean Elab Tactic Parser.Tactic
 
 /-- The `omega` tactic, for resolving integer and natural linear arithmetic problems. -/
 def omegaTactic (cfg : OmegaConfig) : TacticM Unit := do
+  let auxName ← Term.mkAuxName `omega
   liftMetaFinishingTactic fun g => do
     let some g ← g.falseOrByContra | return ()
     g.withContext do
+      let type ← g.getType
+      let g' ← mkFreshExprSyntheticOpaqueMVar type
       let hyps := (← getLocalHyps).toList
       trace[omega] "analyzing {hyps.length} hypotheses:\n{← hyps.mapM inferType}"
-      omega hyps g cfg
+      omega hyps g'.mvarId! cfg
+      -- Omega proofs are typically rather large, so hide them in a separate definition
+      let e ← mkAuxTheorem auxName type (← instantiateMVarsProfiling g') (zetaDelta := true)
+      g.assign e
+
 
 /-- The `omega` tactic, for resolving integer and natural linear arithmetic problems. This
 `TacticM Unit` frontend with default configuration can be used as an Aesop rule, for example via
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 41668d3994..d45e4ff610 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1892,7 +1892,7 @@ def addAutoBoundImplicits' (xs : Array Expr) (type : Expr) (k : Array Expr → E
 
 def mkAuxName (suffix : Name) : TermElabM Name := do
   match (← read).declName? with
-  | none          => throwError "auxiliary declaration cannot be created when declaration name is not available"
+  | none          => Lean.mkAuxName (mkPrivateName (← getEnv) `aux) 1
   | some declName => Lean.mkAuxName (declName ++ suffix) 1
 
 builtin_initialize registerTraceClass `Elab.letrec
diff --git a/tests/lean/run/auxinvariable.lean b/tests/lean/run/auxinvariable.lean
new file mode 100644
index 0000000000..2c01b168ee
--- /dev/null
+++ b/tests/lean/run/auxinvariable.lean
@@ -0,0 +1,18 @@
+/-!
+It used to be that aux theorems could only be created within declarations. But with `omega` wanting
+to create an aux theorem, and `omega` being used in, say, `variable` commands, this is not tenable.
+-/
+
+structure Foo (n : Nat) (h : n > 1 := by omega) : Type
+
+set_option pp.proofs true
+
+/-- info: Foo 3 (Decidable.byContradiction fun a => _check.omega_1 a) : Type -/
+#guard_msgs in
+#check Foo 3
+
+variable (x : Foo 2)
+
+/-- info: x : Foo 2 (Decidable.byContradiction fun a => aux_2 a) -/
+#guard_msgs in
+#check x