diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 14fb6af7d7..e7e6bf8025 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -241,6 +241,11 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
   | nCtx, ctx,       compose d₁ d₂            => return (← formatAux nCtx ctx d₁) ++ (← formatAux nCtx ctx d₂)
   | nCtx, ctx,       group d                  => Format.group <$> formatAux nCtx ctx d
   | nCtx, ctx,       trace data header children => do
+    let childFmts ← children.mapM (formatAux nCtx ctx)
+    if data.cls.isAnonymous then
+      -- Sequence of top-level traces collected by `addTraceAsMessages`, do not indent.
+      return .joinSep childFmts.toList "\n"
+
     let mut msg := f!"[{data.cls}]"
     if data.startTime != 0 then
       msg := f!"{msg} [{data.stopTime - data.startTime}]"
@@ -250,7 +255,6 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
       if maxNum > 0 && children.size > maxNum then
         children := children.take maxNum |>.push <|
           ofFormat f!"{children.size - maxNum} more entries... (increase `maxTraceChildren` to see more)"
-    let childFmts ← children.mapM (formatAux nCtx ctx)
     return .nest 2 (.joinSep (msg::childFmts.toList) "\n")
   | nCtx, ctx?,      ofLazy pp _             => do
     let dyn ← pp (ctx?.map (mkPPContext nCtx))
diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
index 22db50dd6a..2f1b287903 100644
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -380,7 +380,9 @@ def addTraceAsMessages [Monad m] [MonadRef m] [MonadLog m] [MonadTrace m] : m Un
     pos2traces := pos2traces.insert (pos, endPos) <| pos2traces.getD (pos, endPos) #[] |>.push traceElem.msg
   let traces' := pos2traces.toArray.qsort fun ((a, _), _) ((b, _), _) => a < b
   for ((pos, endPos), traceMsg) in traces' do
-    let data := .tagged `trace <| .joinSep traceMsg.toList "\n"
+    -- cmdline and info view differ in how they insert newlines in between trace nodes so we just
+    -- put them in a synthetic root node for now and let the rendering functions handle this case
+    let data := .tagged `trace <| .trace { cls := .anonymous } .nil traceMsg
     logMessage <| Elab.mkMessageCore (← getFileName) (← getFileMap) data .information pos endPos
 
 end Lean
diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean
index b30e64efd7..25d3d02801 100644
--- a/src/Lean/Widget/InteractiveDiagnostic.lean
+++ b/src/Lean/Widget/InteractiveDiagnostic.lean
@@ -149,6 +149,12 @@ where
   | ctx,      compose d₁ d₂            => do let d₁ ← go nCtx ctx d₁; let d₂ ← go nCtx ctx d₂; pure $ d₁ ++ d₂
   | ctx,      group d                  => Format.group <$> go nCtx ctx d
   | ctx,      .trace data header children => do
+    if data.cls.isAnonymous then
+      -- Sequence of top-level traces collected by `addTraceAsMessages`, do not indent.
+      -- As with nested sibling nodes, we do not separate them with newlines but rely on the client
+      -- to never put trace nodes on the same line.
+      return .join (← children.mapM (go nCtx ctx)).toList
+
     let mut header := (← go nCtx ctx header).nest 4
     if data.startTime != 0 then
       header := f!"[{data.stopTime - data.startTime}] {header}"
diff --git a/tests/lean/run/traceFormat.lean b/tests/lean/run/traceFormat.lean
new file mode 100644
index 0000000000..a809bf7662
--- /dev/null
+++ b/tests/lean/run/traceFormat.lean
@@ -0,0 +1,62 @@
+import Lean.CoreM
+
+/-!
+Tests formatting of traces in various combinations, on the cmdline automatically via `#guard_msgs`
+and in the info view via manual testing.
+-/
+
+open Lean
+
+def withNode (cls : Name) (msg : MessageData) (k : CoreM Unit) (collapsed := true) (tag := "") : CoreM Unit := do
+  let oldTraces ← getTraces
+  modifyTraces fun _ => {}
+  k
+  let ref ← getRef
+  let mut data := { cls, collapsed, tag }
+  let msg := .trace data msg ((← getTraces).toArray.map (·.msg))
+  modifyTraces fun _ =>
+    oldTraces.push { ref, msg }
+
+/--
+info: [test] top-level leaf
+[test] top-level leaf
+[test] node with single leaf
+  [test] leaf
+[test] node with adjacent leafs
+  [test] leaf
+  [test] leaf
+[test] nested nodes
+  [test] leaf
+  [test] node
+    [test] leaf
+  [test] leaf
+[test] uncollapsed node
+  [test] leaf
+  [test] node
+    [test] leaf
+  [test] leaf
+[test] node with nested newline
+  [test] line1
+      line2
+-/
+#guard_msgs in
+#eval show CoreM Unit from do
+  addTrace `test "top-level leaf"
+  addTrace `test "top-level leaf"
+  withNode `test "node with single leaf" do
+    addTrace `test "leaf"
+  withNode `test "node with adjacent leafs" do
+    addTrace `test "leaf"
+    addTrace `test "leaf"
+  withNode `test "nested nodes" do
+    addTrace `test "leaf"
+    withNode `test "node" do
+      addTrace `test "leaf"
+    addTrace `test "leaf"
+  withNode `test "uncollapsed node" (collapsed := false) do
+    addTrace `test "leaf"
+    withNode `test "node" do
+      addTrace `test "leaf"
+    addTrace `test "leaf"
+  withNode `test "node with nested newline" do
+    addTrace `test "line1\nline2"