diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean
index f36e65ea1d..79eaeb8f72 100644
--- a/src/Lean/AddDecl.lean
+++ b/src/Lean/AddDecl.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.CoreM
+public import Lean.Meta.Sorry
 public import Lean.Namespace
 public import Lean.Util.CollectAxioms
 
@@ -75,6 +76,28 @@ register_builtin_option warn.sorry : Bool := {
   descr    := "warn about uses of `sorry` in declarations added to the environment"
 }
 
+/--
+If the `warn.sorry` option is set to true and there are no errors in the log already,
+logs a warning if the declaration uses `sorry`.
+-/
+def warnIfUsesSorry (decl : Declaration) : CoreM Unit := do
+  if warn.sorry.get (← getOptions) then
+    if !(← MonadLog.hasErrors) && decl.hasSorry then
+      -- Find an actual sorry expression to use for 'sorry'.
+      -- That way the user can hover over it to see its type and use "go to definition" if it is a labeled sorry.
+      let findSorry : StateRefT (Array (Bool × MessageData)) MetaM Unit := decl.forEachSorryM fun s => do
+        let s' ← addMessageContext s
+        modify fun arr => arr.push (s.isSyntheticSorry, s')
+      let (_, sorries) ← findSorry |>.run #[] |>.run'
+      -- Prefer reporting a synthetic sorry.
+      -- These can appear without logged errors if `decl` is referring to declarations with elaboration errors;
+      -- that's where a user should direct their focus.
+      if let some (_, s) := sorries.find? (·.1) <|> sorries[0]? then
+        logWarning <| .tagged `hasSorry m!"declaration uses '{s}'"
+      else
+        -- This case should not happen, but it ensures a warning will get logged no matter what.
+        logWarning <| .tagged `hasSorry m!"declaration uses 'sorry'"
+
 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
@@ -143,9 +166,7 @@ where
   doAdd := do
     profileitM Exception "type checking" (← getOptions) do
       withTraceNode `Kernel (return m!"{exceptEmoji ·} typechecking declarations {decl.getTopLevelNames}") do
-        if warn.sorry.get (← getOptions) then
-          if !(← MonadLog.hasErrors) && decl.hasSorry then
-            logWarning <| .tagged `hasSorry m!"declaration uses 'sorry'"
+        warnIfUsesSorry decl
         try
           let env ← (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk?
             |> ofExceptKernelException
diff --git a/src/Lean/Meta/Sorry.lean b/src/Lean/Meta/Sorry.lean
index fb28d71971..b9485160f3 100644
--- a/src/Lean/Meta/Sorry.lean
+++ b/src/Lean/Meta/Sorry.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.Data.Lsp.Utf16
+public import Lean.Meta.ForEachExpr
 public import Lean.Meta.InferType
 public import Lean.Util.Recognizers
 
@@ -123,3 +124,42 @@ def isLabeledSorry? (e : Expr) : Option SorryLabelView := do
     guard <| arg.appFn!.appArg!.isAppOfArity ``Unit.unit 0
     let tag ← arg.appArg!.name?
     SorryLabelView.decode? tag
+
+end Meta
+
+/--
+If `e` is a sorry application, returns the sorry itself,
+stripping off any arguments in case the `sorry` is standing in for a function.
+
+For labeled sorries, includes the label information.
+-/
+def Expr.getSorry? (e : Expr) : Option Expr :=
+  if e.isSorry then
+    if (Meta.isLabeledSorry? e).isSome then
+      e.getBoundedAppFn (e.getAppNumArgs - 3)
+    else
+      e.getBoundedAppFn (e.getAppNumArgs - 2)
+  else
+    none
+
+/--
+Evaluates `fn` on each `sorry` in the expression.
+Instantiates bound variables with free variables.
+-/
+def Meta.forEachSorryM {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] (input : Expr)
+    (fn : Expr → m Unit) : m Unit := do
+  Meta.forEachExpr' input fun e => do
+    if let some e' := e.getSorry? then
+      fn e'
+      return false
+    else
+      return true
+
+/--
+Evaluates `fn` on each `sorry` in the declaration.
+-/
+def Declaration.forEachSorryM {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] (decl : Declaration)
+    (fn : Expr → m Unit) : m Unit := do
+  decl.forExprM (Meta.forEachSorryM · fn)
+
+end Lean