diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean
index 0c2bd1620f..d8567fbb8d 100644
--- a/src/Lean/AddDecl.lean
+++ b/src/Lean/AddDecl.lean
@@ -70,6 +70,13 @@ private def looksLikeRelevantTheoremProofType (type : Expr) : Bool :=
   else
     type.isAppOfArity ``WellFounded 2
 
+/-- If `warn.sorry` is set to true, then, so long as the message log does not already have any errors,
+declarations with `sorryAx` generate the "declaration uses 'sorry'" warning. -/
+register_builtin_option warn.sorry : Bool := {
+  defValue := true
+  descr    := "warn about uses of `sorry` in declarations added to the environment"
+}
+
 def addDecl (decl : Declaration) : CoreM Unit := do
   -- register namespaces for newly added constants; this used to be done by the kernel itself
   -- but that is incompatible with moving it to a separate task
@@ -135,8 +142,9 @@ where
   doAdd := do
     profileitM Exception "type checking" (← getOptions) do
       withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getTopLevelNames}") do
-        if !(← MonadLog.hasErrors) && decl.hasSorry then
-          logWarning <| .tagged `hasSorry m!"declaration uses 'sorry'"
+        if warn.sorry.get (← getOptions) then
+          if !(← MonadLog.hasErrors) && decl.hasSorry then
+            logWarning <| .tagged `hasSorry m!"declaration uses 'sorry'"
         try
           let env ← (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk?
             |> ofExceptKernelException
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index b49314d878..8c0c0e7521 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -1155,12 +1155,11 @@ private partial def mkFlatCtor (levelParams : List Name) (params : Array Expr) (
   let ctor := getStructureCtor env structName
   let val ← mkFlatCtorExpr levelParams params ctor replaceIndFVars
   withLCtx {} {} do trace[Elab.structure] "created flat constructor:{indentExpr val}"
-  unless val.hasSyntheticSorry do
-    -- Note: flatCtorName will be private if the constructor is private
-    let flatCtorName := mkFlatCtorOfStructCtorName ctor.name
-    let valType ← replaceIndFVars (← instantiateMVars (← inferType val))
-    let valType := valType.inferImplicit params.size true
-    addDecl <| Declaration.defnDecl (← mkDefinitionValInferrringUnsafe flatCtorName levelParams valType val .abbrev)
+  -- Note: flatCtorName will be private if the constructor is private
+  let flatCtorName := mkFlatCtorOfStructCtorName ctor.name
+  let valType ← replaceIndFVars (← instantiateMVars (← inferType val))
+  let valType := valType.inferImplicit params.size true
+  addDecl <| Declaration.defnDecl (← mkDefinitionValInferrringUnsafe flatCtorName levelParams valType val .abbrev)
 
 private partial def checkResultingUniversesForFields (fieldInfos : Array StructFieldInfo) (u : Level) : TermElabM Unit := do
   for info in fieldInfos do
@@ -1442,13 +1441,16 @@ def elabStructureCommand : InductiveElabDescr where
             finalizeTermElab := withLCtx lctx localInsts do checkDefaults fieldInfos
             prefinalize := fun levelParams params replaceIndFVars => do
               withLCtx lctx localInsts do
-                addProjections params r fieldInfos
+                withOptions (warn.sorry.set · false) do
+                  addProjections params r fieldInfos
                 registerStructure view.declName fieldInfos
                 runStructElabM (init := state) do
-                  mkFlatCtor levelParams params view.declName replaceIndFVars
+                  withOptions (warn.sorry.set · false) do
+                    mkFlatCtor levelParams params view.declName replaceIndFVars
                   addDefaults levelParams params replaceIndFVars
               let parentInfos ← withLCtx lctx localInsts <| runStructElabM (init := state) do
-                mkRemainingProjections levelParams params view
+                withOptions (warn.sorry.set · false) do
+                  mkRemainingProjections levelParams params view
               setStructureParents view.declName parentInfos
               withSaveInfoContext do  -- save new env
                 for field in view.fields do
diff --git a/src/Lean/Util/Sorry.lean b/src/Lean/Util/Sorry.lean
index b97e91c8fb..d7c68de456 100644
--- a/src/Lean/Util/Sorry.lean
+++ b/src/Lean/Util/Sorry.lean
@@ -33,6 +33,9 @@ def Expr.hasNonSyntheticSorry (e : Expr) : Bool :=
 def Declaration.hasSorry (d : Declaration) : Bool := Id.run do
   d.foldExprM (fun r e => r || e.hasSorry) false
 
+def Declaration.hasSyntheticSorry (d : Declaration) : Bool := Id.run do
+  d.foldExprM (fun r e => r || e.hasSyntheticSorry) false
+
 def Declaration.hasNonSyntheticSorry (d : Declaration) : Bool := Id.run do
   d.foldExprM (fun r e => r || e.hasNonSyntheticSorry) false
 
diff --git a/tests/lean/autoImplicitForbidden.lean.expected.out b/tests/lean/autoImplicitForbidden.lean.expected.out
index 0d92b70454..dc28113019 100644
--- a/tests/lean/autoImplicitForbidden.lean.expected.out
+++ b/tests/lean/autoImplicitForbidden.lean.expected.out
@@ -1,7 +1,6 @@
 autoImplicitForbidden.lean:1:8-1:9: error: unknown identifier 'f'
 autoImplicitForbidden.lean:6:10-6:11: error: unknown identifier 'h'
 autoImplicitForbidden.lean:13:24-13:27: error: unknown identifier 'Bla'
-autoImplicitForbidden.lean:14:2-14:5: warning: declaration uses 'sorry'
 autoImplicitForbidden.lean:16:21-16:24: error: unknown identifier 'Foo'
 autoImplicitForbidden.lean:20:18-20:21: error: unknown identifier 'Ex2'
 autoImplicitForbidden.lean:28:14-28:20: error: unknown identifier 'foobar'
diff --git a/tests/lean/run/345.lean b/tests/lean/run/345.lean
index ea558d3aa7..a9bab2c6ef 100644
--- a/tests/lean/run/345.lean
+++ b/tests/lean/run/345.lean
@@ -20,8 +20,6 @@ numerals are polymorphic in Lean, but the numeral `1` cannot be used in a contex
 due to the absence of the instance above
 
 Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
----
-warning: declaration uses 'sorry'
 -/
 #guard_msgs in
 structure Foo where
diff --git a/tests/lean/run/warnSorry.lean b/tests/lean/run/warnSorry.lean
new file mode 100644
index 0000000000..bbd9225293
--- /dev/null
+++ b/tests/lean/run/warnSorry.lean
@@ -0,0 +1,36 @@
+import Lean
+/-!
+# `warn.sorry` tests
+
+When `warn.sorry` is false, don't log the "declaration uses 'sorry'" warning.
+-/
+
+/-- warning: declaration uses 'sorry' -/
+#guard_msgs in
+example : True := sorry
+
+#guard_msgs in
+set_option warn.sorry false in
+example : True := sorry
+
+/-!
+Synthetic sorries should come with associated errors.
+We want to get an error if there is a synthetic sorry with no associated error.
+However: sometimes there are synthetic sorries in terms that come from other other terms
+that have already been warned about. There is no way to tell if a given synthetic sorry had
+been reported on previously. We want to be able to turn off the warning in this case too.
+If we can tell whether sorries have already been warned about,
+we could direct the user to inform us about elaboration bugs (synthetic sorries with no errors in the message log).
+
+So, for now we report them just like a user `sorry`.
+-/
+
+elab "synth_sorry" : term <= expectedType => Lean.Meta.mkSorry expectedType true
+
+/-- warning: declaration uses 'sorry' -/
+#guard_msgs in
+example : True := synth_sorry
+
+#guard_msgs in
+set_option warn.sorry false in
+example : True := synth_sorry