diff --git a/.github/workflows/build_pr.yml b/.github/workflows/build_pr.yml
index b0972ab01..e0f0e3219 100644
--- a/.github/workflows/build_pr.yml
+++ b/.github/workflows/build_pr.yml
@@ -12,6 +12,7 @@ concurrency:
 
 permissions:
   contents: write
+  pull-requests: write
 
 jobs:
   build:
@@ -46,3 +47,18 @@ jobs:
         with:
           name: site
           path: build/
+
+      - name: Check links
+        id: check-links
+        uses: lycheeverse/lychee-action@a8c4c7cb88f0c7386610c35eb25108e448569cb0 # v2.7.0
+        with:
+          args: --no-progress --offline --root-dir $PWD'/build' --exclude '/mathlib4_docs' --exclude '/queueboard' --exclude '/blog' './build/**/*.html'
+          fail: false
+
+      - name: Add comment to PR about link check outcome
+        id: check-links-comment
+        uses: marocchino/sticky-pull-request-comment@773744901bac0e8cbb5a0dc842800d45e9b2b405 # v2.9.4
+        if: steps.check-links.outputs.exit_code != 0
+        with:
+          header: 'Link check errors'
+          path: ./lychee/out.md
diff --git a/make_site.py b/make_site.py
index c9c1b878c..e9676f84b 100755
--- a/make_site.py
+++ b/make_site.py
@@ -408,8 +408,9 @@ def download_N_theorems(kind: NTheorems) -> dict:
                         except KeyError:
                             print(f'Error: {thms} entry {id} refers to a nonexistent declaration {decl}')
                             continue
-                        # note: the `header-data.json` data file uses doc-relative links
-                        header = decl_info.header.replace('href="./Mathlib/', 'href="./mathlib4_docs/Mathlib/')
+                        # note: the `header-data.json` data file uses doc-relative links;
+                        # rewrite all of them to point into the mathlib4_docs subdirectory
+                        header = decl_info.header.replace('href="./', 'href="./mathlib4_docs/')
                         doc_decls.append(DocDecl(
                             name=decl,
                             decl_header_html = header,
diff --git a/templates/glossary.md b/templates/glossary.md
index db3f581bf..7bf4016f0 100644
--- a/templates/glossary.md
+++ b/templates/glossary.md
@@ -373,7 +373,7 @@ Good `simp` lemmas guide the `simp` tactic towards reducing complex expressions
 
 A convention within [Mathlib](#Mathlib) for expressing propositions with multiple equivalent forms in a single conventional one.
 
-Examples and further detail can be found on [the `simp` page](simp.html#simp-normal-form).
+Examples and further detail can be found on [the `simp` page](extras/simp.html#simp-normal-form).
 
 ### syntax linter