diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml
new file mode 100644
index 0000000..f61c0c4
--- /dev/null
+++ b/.github/workflows/update.yml
@@ -0,0 +1,36 @@
+name: Update Lean toolchain and pinned deps
+
+on:
+  schedule:
+    # Daily at 00:00 UTC
+    - cron: "0 0 * * *"
+  workflow_dispatch:
+
+permissions:
+  contents: write
+  pull-requests: write
+
+jobs:
+  update:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+
+      # Mint a token from the GitHub App so the opened PR triggers CI; pushes
+      # made with GITHUB_TOKEN do not. Same App as the org repo-sync workflows.
+      - uses: actions/create-github-app-token@v3
+        id: app-token
+        with:
+          client-id: ${{ secrets.TOKEN_APP_ID }}
+          private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }}
+
+      # `dev` carries the fork's bump_mode/release_channel support; `main` only
+      # mirrors upstream, which silently ignores these inputs. A PR is opened
+      # on an update/lean-{release} branch whether or not the build passes, so
+      # an incompatible release shows up as a failing PR to review.
+      - uses: argumentcomputer/lean-update@dev
+        with:
+          bump_mode: pinned-tags
+          on_update_fails: pr
+          build_args: "--wfail"
+          token: ${{ steps.app-token.outputs.token }}
diff --git a/lake-manifest.json b/lake-manifest.json
index 8351540..6f005e3 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -8,7 +8,7 @@
    "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "6304553",
+   "inputRev": "v4.31.0",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "LSpec",
diff --git a/lakefile.toml b/lakefile.toml
index 893c2e9..3ba5ef4 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -6,7 +6,7 @@ testDriver = "tests"
 [[require]]
 name = "plausible"
 git = "https://github.com/leanprover-community/plausible"
-rev = "6304553"
+rev = "v4.31.0"
 
 [[lean_lib]]
 name = "LSpec"