diff --git a/doc/UsersGuide/Releases/Assemble.lean b/doc/UsersGuide/Releases/Assemble.lean
index 318a3e47..ea9af9ab 100644
--- a/doc/UsersGuide/Releases/Assemble.lean
+++ b/doc/UsersGuide/Releases/Assemble.lean
@@ -97,13 +97,13 @@ public def bucket
       if hasSection entry then
         -- The entry's own metadata is kept; only its permalink comes from the release note.
         some { entry with
-          metadata := some { entry.metadata.getD {} with tag := some (metadata.tag : Manual.Tag) },
+          metadata := some { entry.metadata.getD {} with tag := some metadata.tag },
           content := entry.content.extract 1 }
       else none
     some <| Part.mk
       #[Inline.text title]
       title
-      (some { tag := some (tag : Manual.Tag) })
+      (some { tag := some tag })
       #[ Doc.Block.other
            (Block.release (toString version) { title, version })
            #[],
@@ -252,7 +252,7 @@ private def summaryTags (part : Part Manual) : Array (Option String) :=
   (bucket ⟨4, 33, 0⟩ false #[(testMetadata, entry)]).any fun part =>
     part.subParts.all fun s =>
       (s.metadata.map (·.draft)).getD false &&
-      (s.metadata.bind (·.tag)) == some ("entry" : Manual.Tag)
+      (s.metadata.bind (·.tag)) == some "entry"
 
 end Tests
 
diff --git a/src/multi-verso/MultiVerso.lean b/src/multi-verso/MultiVerso.lean
index 70fe016b..5f3ac028 100644
--- a/src/multi-verso/MultiVerso.lean
+++ b/src/multi-verso/MultiVerso.lean
@@ -285,6 +285,12 @@ public instance : GetElem? RefDomain String (Array RefObject) fun dom name => na
   getElem dom name ok := dom.contents[name]'ok
   getElem? dom name := dom.contents[name]?
 
+/--
+Returns the canonical names used in {name}`domain`, in sorted order.
+-/
+public def RefDomain.canonicalNames (domain : RefDomain) : Array String :=
+  domain.contents.keysArray.qsortOrd
+
 private def RefDomain.structEq (x y : RefDomain) :=
   let ⟨t1, d1, c1⟩ := x
   let ⟨t2, d2, c2⟩ := y
diff --git a/src/tests/Tests/Tags.lean b/src/tests/Tests/Tags.lean
index 18c19fa8..f75eb58d 100644
--- a/src/tests/Tests/Tags.lean
+++ b/src/tests/Tests/Tags.lean
@@ -5,6 +5,7 @@ Author: David Thrane Christiansen
 -/
 module
 import VersoManual
+meta import VersoManual
 
 set_option doc.verso true
 
@@ -94,4 +95,171 @@ info: (false, some "my-tag", none, true)
     pure (tag, machine, chosen)
   pure (tag.isSome, htmlId state machine, htmlId state chosen, failed)
 
+/-
+A name containing a space gives the element its slug as an HTML id.
+-/
+/-- info: (true, some "some-tag", false) -/
+#guard_msgs in
+#eval show IO _ from do
+  let ((tag, id), state, failed) ← run do
+    let id ← freshId
+    let tag ← providedTag id #["page"] "some tag"
+    pure (tag, id)
+  pure (tag.isSome, htmlId state id, failed)
+
+/-
+Names that share a slug are duplicates, because both need the same HTML id. The error names the
+slug when it differs from the name as written.
+-/
+/--
+info: Duplicate tag 'some tag': its slug 'some-tag' is already in use
+An error was encountered!
+---
+info: (false, some "some-tag", none, true)
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let ((tag, first, second), state, failed) ← run do
+    let first ← freshId
+    let second ← freshId
+    let _ ← providedTag first #["page"] "some-tag"
+    let tag ← providedTag second #["page"] "some tag"
+    pure (tag, first, second)
+  pure (tag.isSome, htmlId state first, htmlId state second, failed)
+
+/--
+info: Duplicate tag 'some-tag'
+An error was encountered!
+---
+info: (false, some "some-tag", none, true)
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let ((tag, first, second), state, failed) ← run do
+    let first ← freshId
+    let second ← freshId
+    let _ ← providedTag first #["page"] "some tag"
+    let tag ← providedTag second #["page"] "some-tag"
+    pure (tag, first, second)
+  pure (tag.isSome, htmlId state first, htmlId state second, failed)
+
+/-! Tests for assigning tags to parts with {name}`tagPart`. -/
+
+/--
+Runs a traversal action with no extensions against an empty state and context, returning its
+result, the resulting state, and whether any errors were logged.
+-/
+private def runTraverse (act : TraverseM α) : IO (α × TraverseState × Bool) := do
+  let logger ← Logger.new
+  let (result, state) ←
+    (TraverseM.run (ExtensionImpls.fromLists [] []) {} (TraverseState.initialize {}) act).run logger
+  let failed ← logger.failIfErrors
+  return (result, state, failed != 0)
+
+/-
+Traversal registers a part in the section domain under its name exactly as written, resolvable by
+{name}`TraverseState.resolveDomainObject`, while its HTML id is the slug. The name in the part's
+metadata is untouched.
+-/
+/-- info: (some "some tag", some "some-tag", true, some "some-tag", false) -/
+#guard_msgs in
+#eval show IO _ from do
+  let ((name, id), state, failed) ← runTraverse do
+    let id ← freshId
+    let md : PartMetadata := { tag := some "some tag", id := some id }
+    let part : Doc.Part Manual := .mk #[Doc.Inline.text "Some Tag"] "Some Tag" (some md) #[] #[]
+    -- Two rounds, as the traversal driver would run them
+    let t ← tagPart part md (·.id) (·.xrefTag) (·.tag) savePartXref
+    let md := { md with xrefTag := some t }
+    let _ ← tagPart part md (·.id) (·.xrefTag) (·.tag) savePartXref
+    pure (md.tag, id)
+  let resolved :=
+    match state.resolveDomainObject sectionDomain "some tag" with
+    | .ok link => some link.htmlId.toString
+    | .error _ => none
+  pure (name, htmlId state id,
+    (state.getDomainObject? sectionDomain "some-tag").isNone, resolved, failed)
+
+/-
+Two parts that claim the same name produce a single, readable duplicate error.
+-/
+/--
+info: Duplicate tag 'some tag': its slug 'some-tag' is already in use
+An error was encountered!
+---
+info: true
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let (_, _, failed) ← runTraverse do
+    let first ← freshId
+    let md1 : PartMetadata := { tag := some "some tag", id := some first }
+    let part1 : Doc.Part Manual := .mk #[Doc.Inline.text "A"] "A" (some md1) #[] #[]
+    let _ ← tagPart part1 md1 (·.id) (·.xrefTag) (·.tag) savePartXref
+    let second ← freshId
+    let md2 : PartMetadata := { tag := some "some tag", id := some second }
+    let part2 : Doc.Part Manual := .mk #[Doc.Inline.text "B"] "B" (some md2) #[] #[]
+    let _ ← tagPart part2 md2 (·.id) (·.xrefTag) (·.tag) savePartXref
+  pure failed
+
+/-! Tests for suggesting alternatives to unresolved cross-references. -/
+
+/-- info: "" -/
+#guard_msgs in
+#eval suggestRefTargets #["alpha", "beta"] "zzzzzzzzzzzz"
+
+/-- info: "\nDid you mean one of these?\n * 'some tag'\n * 'some-tag'" -/
+#guard_msgs in
+#eval suggestRefTargets #["some-tag", "some tag", "other"] "some tg"
+
+/-
+At most five targets are suggested.
+-/
+/-- info: "\nDid you mean one of these?\n * 'tag1'\n * 'tag2'\n * 'tag3'\n * 'tag4'\n * 'tag5'" -/
+#guard_msgs in
+#eval suggestRefTargets #["tag6", "tag5", "tag4", "tag3", "tag2", "tag1"] "tag"
+
+/-! Tests for the unresolved-reference error message with {name}`unresolvedRefMessage`. -/
+
+/-
+A name that is absent from the domain gets suggestions of nearby names.
+-/
+/--
+info: "No destination found for tag 'some tg' in Verso.Genre.Manual.section\nDid you mean one of these?\n * 'some tag'"
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let (_, state, _) ← runTraverse do
+    let id ← freshId
+    modify (·.saveDomainObject sectionDomain "some tag" id)
+  pure (unresolvedRefMessage state none "some tg")
+
+/-
+A name that is present in the domain failed to resolve for another reason, which the message
+states instead of suggesting the name to itself.
+-/
+/--
+info: "Ref some tag in Verso.Genre.Manual.section has 2 targets, can only link to one"
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let (_, state, _) ← runTraverse do
+    let first ← freshId
+    let second ← freshId
+    modify (·.saveDomainObject sectionDomain "some tag" first
+      |>.saveDomainObject sectionDomain "some tag" second)
+  pure (unresolvedRefMessage state none "some tag")
+
+/-
+A name whose domain object has no targets at all, which happens when only data was saved for it.
+-/
+/--
+info: "No link target registered for some tag in Verso.Genre.Manual.section"
+-/
+#guard_msgs in
+#eval show IO _ from do
+  let (_, state, _) ← runTraverse do
+    modify (·.saveDomainObjectData sectionDomain "some tag" .null)
+  pure (unresolvedRefMessage state none "some tag")
+
 end Verso.Tests.Tags
diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean
index 62ca5ee3..10707cce 100644
--- a/src/verso-manual/VersoManual.lean
+++ b/src/verso-manual/VersoManual.lean
@@ -17,6 +17,7 @@ public import Verso.Output.Html.ElasticLunr
 public import Verso.Doc.Lsp
 public import Verso.Doc.Elab
 public import Verso.FS
+public import Verso.SmartSuggestions
 
 public import VersoSearch
 public import VersoSearch.DomainSearch
@@ -84,6 +85,34 @@ deriving BEq, ToJson, FromJson
 defmethod Part.htmlToc (part : Part Manual) : Bool :=
   part.metadata.map (·.htmlToc) |>.getD true
 
+/--
+Renders the names among {name}`candidates` that are close to {name}`name`, as a suffix for the
+error message about an unresolved cross-reference. Returns the empty string when no candidate is
+close enough.
+-/
+def suggestRefTargets (candidates : Array String) (name : String) : String :=
+  let suggestions := smartSuggestions candidates name (count := 5)
+  if suggestions.isEmpty then ""
+  else suggestions.foldl (init := "\nDid you mean one of these?") (· ++ s!"\n * '{·}'")
+
+/--
+The error message for a cross-reference to {name}`name` that traversal could not resolve.
+
+When the name is absent from the domain, nearby names from the domain's contents in {name}`st`
+are suggested. When the name is present, resolution failed for another reason, such as the name
+having multiple targets. The resulting message preserves this.
+-/
+def unresolvedRefMessage (st : TraverseState) (domain : Option Name) (name : String) : String :=
+  let domain := domain.getD sectionDomain
+  if (st.getDomainObject? domain name).isSome then
+    match st.resolveDomainObject domain name with
+    | .error e => e
+    | .ok _ =>
+      s!"'{name}' in {domain} was not resolved during traversal; the document may need more traversal passes"
+  else
+    let candidates := st.domains[domain]?.map (·.canonicalNames) |>.getD #[]
+    s!"No destination found for tag '{name}' in {domain}{suggestRefTargets candidates name}"
+
 inline_extension Inline.ref (canonicalName : String) (domain : Option Name) (remote : Option String) (resolvedDestination : Option Link := none) where
   data := ToJson.toJson (RefInfo.mk canonicalName domain remote resolvedDestination)
   traverse := fun _ info content => do
@@ -108,7 +137,7 @@ inline_extension Inline.ref (canonicalName : String) (domain : Option Name) (rem
       | .error e =>
         reportError e; content.mapM go
       | .ok { canonicalName := name, domain, remote := none, resolvedDestination := none } =>
-        reportError ("No destination found for tag '" ++ name ++ "' in " ++ toString domain); content.mapM go
+        reportError (unresolvedRefMessage (← Doc.TeX.state) domain name); content.mapM go
       | .ok { canonicalName := name, domain, remote := some remote, resolvedDestination := none } =>
         reportError ("No destination found for remote '" ++ remote ++ "' tag '" ++ name ++ "' in " ++ toString domain); content.mapM go
       | .ok {resolvedDestination := some dest, remote, ..} =>
@@ -127,7 +156,7 @@ inline_extension Inline.ref (canonicalName : String) (domain : Option Name) (rem
       | .error e =>
         reportError e; content.mapM go
       | .ok { canonicalName := name, domain, remote := none, resolvedDestination := none } =>
-        reportError ("No destination found for tag '" ++ name ++ "' in " ++ toString domain); content.mapM go
+        reportError (unresolvedRefMessage (← Doc.Html.HtmlT.state) domain name); content.mapM go
       | .ok { canonicalName := name, domain, remote := some remote, resolvedDestination := _ } =>
         let domain := domain |>.getD sectionDomain
         let remoteData ← readThe AllRemotes
@@ -141,7 +170,7 @@ inline_extension Inline.ref (canonicalName : String) (domain : Option Name) (rem
               else
                 let dests := objs.map (s!" * {·.link.link}") |>.toList |> "\n".intercalate
                 reportError s!"Remote '{remote}' domain '{domain}' contains multiple destinations for '{name}':\n{dests}"
-            else reportError s!"Remote '{remote}' contains domain '{domain}, but it not item '{name}'"
+            else reportError s!"Remote '{remote}' contains domain '{domain}', but not item '{name}'{suggestRefTargets dom.canonicalNames name}"
           else reportError s!"Remote '{remote}' does not contain domain '{domain}' (looking up '{name}')"
         else reportError s!"Remote '{remote}' not found for tag '{name}' in domain '{domain}'"
         -- If any error was logged, just don't emit a link
diff --git a/src/verso-manual/VersoManual/Basic.lean b/src/verso-manual/VersoManual/Basic.lean
index 92721f64..deb3798a 100644
--- a/src/verso-manual/VersoManual/Basic.lean
+++ b/src/verso-manual/VersoManual/Basic.lean
@@ -220,8 +220,20 @@ structure PartMetadata where
   authorshipNote : Option String := none
   /-- The publication date -/
   date : Option String := none
-  /-- The main tag for the part, used for cross-references. -/
-  tag : Option Tag := none
+  /--
+  This part's canonical name.
+
+  The canonical name is used for stable cross references. It also serves as the basis
+  for the section's HTML ID.
+  -/
+  tag : Option String := none
+  /--
+  This part's cross-referencing tag.
+
+  This field is set during traversal, which derives a unique external tag from the part's
+  canonical name.
+  -/
+  xrefTag : Option Tag := none
   /-- If this part ends up as the root of a file, use this name for it -/
   file : Option String := none
   /-- The internal unique ID, which is automatically assigned during traversal. -/
@@ -1072,7 +1084,10 @@ def providedTag [Monad m] [MonadState TraverseState m] [MonadBuildLog m]
   if let some id' := (← get).tags[tag]? then
     if id' != id then
       -- Another element holds this tag, so this one is left without an external tag.
-      reportError s!"Duplicate tag '{name}'"
+      if slug.toString == name then
+        reportError s!"Duplicate tag '{name}'"
+      else
+        reportError s!"Duplicate tag '{name}': its slug '{slug.toString}' is already in use"
       return none
   modify fun st => { st with
     tags := st.tags.insert tag id,
@@ -1376,7 +1391,7 @@ def ancestorSearchPriority (headers : Array PartHeader) : Int :=
     let p : Int := (h.metadata.map (·.searchPriority.val) |>.getD 50 : Nat)
     acc + (p - 50)
 
-def savePartXref (slug : Slug) (id : InternalId) (part : Part Manual) : TraverseM Unit := do
+def savePartXref (name : String) (id : InternalId) (part : Part Manual) : TraverseM Unit := do
   let jsonMetadata :=
     Json.arr ((← read).inPart part |>.headers.map (fun h => json%{
       "title": $h.titleString,
@@ -1392,7 +1407,7 @@ def savePartXref (slug : Slug) (id : InternalId) (part : Part Manual) : Traverse
     ((← read).inPart part |>.headers[1:]).toArray.map (fun (h : PartHeader) => h.metadata.bind (·.assignedNumber))
       |>.mapM _root_.id |>.map sectionNumberString
   let searchPriority := ancestorSearchPriority ((← read).inPart part |>.headers)
-  modify fun (st : TraverseState) => st.saveDomainObject sectionDomain slug.toString id |>.saveDomainObjectData sectionDomain slug.toString (json%{
+  modify fun (st : TraverseState) => st.saveDomainObject sectionDomain name id |>.saveDomainObjectData sectionDomain name (json%{
     "context": $jsonMetadata,
     "title": $title,
     "shortTitle": $shortTitle,
@@ -1403,25 +1418,26 @@ def savePartXref (slug : Slug) (id : InternalId) (part : Part Manual) : Traverse
 /--
 Assigns a tag to a part during traversal.
 
-This operation is careful to preserve and prioritize user-selected tags. In the first round, the
+This operation is careful to preserve and prioritize user-chosen names. In the first round, the
 following may occur:
 
- * If there's no tag at all, then an internal tag is applied.
+ * If the part has a name (from {name}`getName`), its provided tag is converted to a unique
+   external tag whose slug becomes the part's HTML id.
 
- * If there's a provided tag, it is converted to an external tag and added as an xref target.
+ * If the part has no name at all, then an internal tag is applied.
 
 In subsequent rounds, the internal tags are converted to external tags. At this point, the
-user-provided tags have already been made external. It also ensures that auto-generated tags are
-never added as xref targets.
+tags based on the user's {name (full := PartMetadata.tag)}`tag` field have already been made
+external.
 -/
 def tagPart
     (part : Lean.Doc.Part Manual.Inline Manual.Block m) (metadata : m)
-    (getId : m → Option InternalId) (getTag : m → Option Tag)
-    (saveXref : Slug → InternalId → Lean.Doc.Part Manual.Inline Manual.Block m → TraverseM Unit) :
+    (getId : m → Option InternalId) (getTag : m → Option Tag) (getName : m → Option String)
+    (saveXref : String → InternalId → Lean.Doc.Part Manual.Inline Manual.Block m → TraverseM Unit) :
     TraverseM Tag := do
   let some id := getId metadata
     | reportError "No internal ID assigned while tagging part"; return default
-  match getTag metadata with
+  match getTag metadata <|> (getName metadata).map .provided with
   | none =>
     -- Assign an internal tag - the next round will make it external. This is done in two rounds to
     -- give priority to user-provided tags that might otherwise anticipate the name-mangling scheme
@@ -1432,13 +1448,14 @@ def tagPart
     -- Ensure uniqueness
     if let some id' := (← get).tags[t]? then
       if id != id' then
-        reportError s!"Duplicate tag '{t}'"
+        unless t matches Tag.provided _ do
+          reportError s!"Duplicate tag '{t}'"
     else
       modify fun st => {st with tags := st.tags.insert t id}
     let path := (← readThe TraverseContext).path
     match t with
     | Tag.external name =>
-      saveXref name id { part with metadata := some metadata }
+      saveXref ((getName metadata).getD name.toString) id { part with metadata := some metadata }
       -- These are the actual IDs to use in generated HTML and links and such
       modify fun st : TraverseState => { st with externalTags := st.externalTags.insert id { path, htmlId := name } }
       return t
@@ -1462,7 +1479,7 @@ instance : Traverse Manual TraverseM where
     «meta» := { «meta» with id := some id }
 
     -- Next, assign a tag, prioritizing user-chosen external IDs
-    «meta» := { «meta» with tag := ← tagPart part «meta» (·.id) (·.tag) savePartXref }
+    «meta» := { «meta» with xrefTag := ← tagPart part «meta» (·.id) (·.xrefTag) (·.tag) savePartXref }
 
     -- Assign section numbers to subsections
     let mut i := 1
@@ -1581,6 +1598,9 @@ def permalink (id : InternalId) (st : TraverseState) (inline : Bool := true) : H
     -- If there's multiple, select one arbitrarily.
     let (domain, canonicalName) := candidates[0]
     let classes := "permalink-widget " ++ if inline then "inline" else "block"
+    -- The names may contain characters with meaning in URLs, such as spaces or ampersands.
+    let domain := System.Uri.escapeUri (toString domain)
+    let canonicalName := System.Uri.escapeUri canonicalName
     {{<span class={{classes}}>
         <a href=s!"/find/?domain={domain}&name={canonicalName}" title="Permalink">"🔗"</a>
       </span>
diff --git a/src/verso-manual/VersoManual/Glossary.lean b/src/verso-manual/VersoManual/Glossary.lean
index 723035fe..ec064c9c 100644
--- a/src/verso-manual/VersoManual/Glossary.lean
+++ b/src/verso-manual/VersoManual/Glossary.lean
@@ -248,7 +248,7 @@ public def tech.descr : InlineDescr where
               content.mapM go
           else
             let keys := remote.domains[technicalTermDomain]?
-              |>.map (·.contents.keysArray.qsortOrd.toList |> ", ".intercalate)
+              |>.map (·.canonicalNames.toList |> ", ".intercalate)
               |>.map ("Keys are: " ++ ·)
               |>.getD "Technical term domain not found."
             reportError s!"No term def with key \"{key}\" in remote {r.quote}. {keys}" loc
diff --git a/src/verso-tutorial/VersoTutorial/Basic.lean b/src/verso-tutorial/VersoTutorial/Basic.lean
index 8689668d..bef18bb9 100644
--- a/src/verso-tutorial/VersoTutorial/Basic.lean
+++ b/src/verso-tutorial/VersoTutorial/Basic.lean
@@ -58,8 +58,20 @@ deriving BEq, Hashable, DecidableEq, Inhabited, Repr, ToJson, FromJson
 open Manual (Tag InternalId) in
 /-- Metadata on tutorials. -/
 structure Tutorial.PartMetadata where
-  /-- The main tag for the part, used for cross-references. -/
-  tag : Option Tag := none
+  /--
+  This part's canonical name.
+
+  The canonical name is used for stable cross references. It also serves as the basis
+  for the section's HTML ID.
+  -/
+  tag : Option String := none
+  /--
+  This part's cross-referencing tag.
+
+  This field is set during traversal, which derives a unique external tag from the part's
+  canonical name.
+  -/
+  xrefTag : Option Tag := none
   /-- Use this filename component in the URL. -/
   slug : String
   /-- The internal unique ID, which is automatically assigned during traversal. -/
@@ -142,7 +154,7 @@ instance : TraverseBlock Tutorial where
 /--
 Saves a cross-reference to a part to the section domain.
 -/
-def savePartXref (slug : Slug) (id : InternalId) (part : Part Tutorial) : Manual.TraverseM Unit := do
+def savePartXref (name : String) (id : InternalId) (part : Part Tutorial) : Manual.TraverseM Unit := do
   let jsonMetadata :=
     Json.arr (TraversePart.inPart part (← read) |>.headers.map (fun h => json%{
       "title": $h.titleString
@@ -150,8 +162,8 @@ def savePartXref (slug : Slug) (id : InternalId) (part : Part Tutorial) : Manual
   let title := TraversePart.inPart part (← read) |>.headers |>.back? |>.map (·.titleString)
 
   modify fun (st : Manual.TraverseState) =>
-    st.saveDomainObject Manual.sectionDomain slug.toString id
-      |>.saveDomainObjectData Manual.sectionDomain slug.toString (json%{
+    st.saveDomainObject Manual.sectionDomain name id
+      |>.saveDomainObjectData Manual.sectionDomain name (json%{
         "context": $jsonMetadata,
         "title": $title,
         "shortTitle": null,
@@ -203,7 +215,7 @@ instance : Traverse Tutorial TraverseM where
     «meta» := { «meta» with id := some id }
 
     -- Next, assign a tag, prioritizing user-chosen external IDs.
-    «meta» := { «meta» with tag := ← tagPart part «meta» (·.id) (·.tag) savePartXref }
+    «meta» := { «meta» with xrefTag := ← tagPart part «meta» (·.id) (·.xrefTag) (·.tag) savePartXref }
 
     -- Traverse the metadata's description
     «meta» := { «meta» with summary := ← withReader (TraversePart.inPart part) <| Genre.traverseInline Manual «meta».summary }
diff --git a/src/verso/Verso.lean b/src/verso/Verso.lean
index 6e09efd1..f7195352 100644
--- a/src/verso/Verso.lean
+++ b/src/verso/Verso.lean
@@ -33,5 +33,6 @@ public import Verso.Output.Html.CssVars
 public import Verso.Output.Html.ElasticLunr
 public import Verso.Output.Html.KaTeX
 public import Verso.Output.TeX
+public import Verso.SmartSuggestions
 public import Verso.SyntaxUtils
 public import Verso.WithoutAsync
diff --git a/src/verso/Verso/Code/External.lean b/src/verso/Verso/Code/External.lean
index 0757a4e8..29046b26 100644
--- a/src/verso/Verso/Code/External.lean
+++ b/src/verso/Verso/Code/External.lean
@@ -20,6 +20,7 @@ public meta import Verso.ExpectString
 public meta import Verso.Doc.Suggestion
 public meta import Verso.Hint
 public meta import Verso.Log
+public meta import Verso.SmartSuggestions
 
 import SubVerso.Highlighting
 public meta import SubVerso.Examples.Messages
@@ -76,31 +77,6 @@ Adds a newline to a string if it doesn't already end with one.
 -/
 public meta def withNl (s : String) : String := if s.endsWith "\n" then s else s ++ "\n"
 
-/--
-Default suggestion threshold function: a suggestion is sufficiently close if
- * the input is shorter than 5 and their Levenshtein distance is 1 or less,
- * the input is shorter than 10 and their distance is 2 or less, or
- * the distance is shorter than 3.
--/
-meta def suggestionThreshold (input _candidate : String) := if input.length < 5 then 1 else if input.length < 10 then 2 else 3
-
-/--
-Adds up to {name}`count` suggestions.
-
-{name}`candidates` are the valid inputs and {name}`input` is the provided input. Suggestions are added if
-they are "sufficiently close" to the input, as determined by {name}`threshold`.
--/
-meta def smartSuggestions (candidates : Array String) (input : String) (count : Nat := 10) (threshold := suggestionThreshold) : Array String :=
-  let toks := candidates.filterMap fun t =>
-    let limit := threshold input t
-    EditDistance.levenshtein t input limit <&> (t, ·)
-  let toks := toks.qsort (fun x y => x.2 < y.2 || (x.2 == y.2 && x.1 < y.1))
-  let toks := toks.take count
-  -- TODO test thresholds/sorting
-  toks.map fun (t, _) => t
-
-
-
 /--
 Loads the contents of a module, parsed by anchor. The results are cached.
 -/
diff --git a/src/verso/Verso/SmartSuggestions.lean b/src/verso/Verso/SmartSuggestions.lean
new file mode 100644
index 00000000..4a5ef7a9
--- /dev/null
+++ b/src/verso/Verso/SmartSuggestions.lean
@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+module
+
+import Lean.Data.EditDistance
+
+set_option doc.verso true
+
+/-!
+Suggestions of valid alternatives to invalid inputs, ranked by edit distance.
+-/
+
+namespace Verso
+
+open Lean
+
+/--
+Default suggestion threshold function: a suggestion is sufficiently close if
+ * the input is shorter than 5 and their Levenshtein distance is 1 or less,
+ * the input is shorter than 10 and their distance is 2 or less, or
+ * the distance is shorter than 3.
+-/
+public def suggestionThreshold (input _candidate : String) := if input.length < 5 then 1 else if input.length < 10 then 2 else 3
+
+/--
+Adds up to {name}`count` suggestions.
+
+{name}`candidates` are the valid inputs and {name}`input` is the provided input. Suggestions are added if
+they are "sufficiently close" to the input, as determined by {name}`threshold`.
+-/
+public def smartSuggestions (candidates : Array String) (input : String) (count : Nat := 10) (threshold := suggestionThreshold) : Array String :=
+  let toks := candidates.filterMap fun t =>
+    let limit := threshold input t
+    EditDistance.levenshtein t input limit <&> (t, ·)
+  let toks := toks.qsort (fun x y => x.2 < y.2 || (x.2 == y.2 && x.1 < y.1))
+  let toks := toks.take count
+  -- TODO test thresholds/sorting
+  toks.map fun (t, _) => t
+
+end Verso
diff --git a/static-web/find.js b/static-web/find.js
index 7ffbbb62..4e61b321 100644
--- a/static-web/find.js
+++ b/static-web/find.js
@@ -28,6 +28,46 @@ let paramName = params.get("name");
 
 let xref = /** @type {{xref: XRef}} */ (/** @type {unknown} */ (window)).xref;
 
+/**
+ * The replacements for characters that are not valid in slugs. This mirrors the mangling table in
+ * MultiVerso.Slug.
+ * @type {Record<string, string>}
+ */
+const slugReplacements = {
+    "<": "_LT_",
+    ">": "_GT_",
+    ";": "_SEMI_",
+    "‹": "_FLQ_",
+    "›": "_FRQ_",
+    "«": "_FLQQ_",
+    "»": "_FLQQ_",
+    "⟨": "_LANGLE_",
+    "⟩": "_RANGLE_",
+    "(": "_LPAR_",
+    ")": "_RPAR_",
+    "[": "_LSQ_",
+    "]": "_RSQ_",
+    "→": "_ARR_",
+    "↦": "_MAPSTO_",
+    "⊢": "_VDASH_",
+};
+
+/**
+ * Converts a string to a valid slug, mangling as appropriate. This mirrors the slug computation in
+ * MultiVerso.Slug, so names can be compared with links that were minted from their slugs.
+ * @param {string} s
+ * @returns {string}
+ */
+function sluggify(s) {
+    let out = "";
+    for (const c of s) {
+        if (/^[a-zA-Z0-9_-]$/.test(c)) out += c;
+        else if (c === " " || c === "\t" || c === "\r" || c === "\n") out += "-";
+        else out += slugReplacements[c] ?? "___";
+    }
+    return out;
+}
+
 if (paramName) {
     /**
      * @type (Item & {domain: string})[]
@@ -57,6 +97,27 @@ if (paramName) {
         }
     }
 
+    if (options.length == 0) {
+        // Permalinks from before a bug fix that separated sections' HTML IDs from their
+        // canonical names in the section domain were mangled as slugs. If we don't find
+        // any results, we try to recover by checking equality modulo sluggification.
+        // This workaround was introduced in August 2026 and should be removed when it
+        // seems unlikely for old permalinks to be a significant problem.
+        const nameSlug = sluggify(paramName);
+        const searchDomains = domains && domains.length > 0 ? domains : Object.keys(xref);
+        for (const domain of searchDomains) {
+            if (!xref.hasOwnProperty(domain)) continue;
+            const contents = xref[domain]["contents"];
+            for (const key of Object.keys(contents)) {
+                if (sluggify(key) === nameSlug) {
+                    for (const i of contents[key]) {
+                        options.push(Object.assign(i, { domain: domain }));
+                    }
+                }
+            }
+        }
+    }
+
     if (options.length == 0) {
         addEventListener("DOMContentLoaded", (_event) => {
             document.title = "Not found: '" + paramName + "'";