From 5f15d413caf98736e1ca8d372190255c5c0bbc87 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Fri, 25 Sep 2026 14:04:48 +1000
Subject: [PATCH 1/2] chore: bump toolchain to v4.34.1

Move from v4.34.0 to v4.34.1, which carries runtime fixes, and repin mathlib
and doc-gen4 at their v4.34.1 tags. No source changes: `lake build` is clean
(9589 jobs).

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 lake-manifest.json | 8 ++++----
 lakefile.toml      | 4 ++--
 lean-toolchain     | 2 +-
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index a5df238c0..f864b8e3c 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5ed2965256430c3649e86755f9576b54eca72435",
+   "rev": "d13f23b723b8a846827a245b89c10fc7d3f11612",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.34.0",
+   "inputRev": "v4.34.1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a6521b2d0c93dcdf2d640089f95548df5dd8bf46",
+   "rev": "953c8992d174b4e56955e01e101d46668c68f2bb",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.34.0",
+   "inputRev": "v4.34.1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
diff --git a/lakefile.toml b/lakefile.toml
index d3c52e482..2855831ab 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -11,12 +11,12 @@ defaultTargets = ["Physlib", "QuantumInfo"]
 [[require]]
 name = "«doc-gen4»"
 git = "https://github.com/leanprover/doc-gen4"
-rev = "v4.34.0"
+rev = "v4.34.1"
 
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.34.0"
+rev = "v4.34.1"
 
 [[lean_lib]]
 name = "Physlib"
diff --git a/lean-toolchain b/lean-toolchain
index 12359f928..ba8ebf2db 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.34.0
+leanprover/lean4:v4.34.1

From b99df446f7a56b9d8574c040bf9faafcd7dc0151 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 25 Sep 2026 05:44:28 +0100
Subject: [PATCH 2/2] docs: update readme

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 9a9a0e143..acc7bc547 100644
--- a/README.md
+++ b/README.md
@@ -18,7 +18,7 @@
 
 
 [![](https://img.shields.io/badge/View_The-Stats-blue)](https://physlib.io/Stats)
-[![](https://img.shields.io/badge/Lean-v4.34.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.34.0)
+[![](https://img.shields.io/badge/Lean-v4.34.1-blue)](https://github.com/leanprover/lean4/releases/tag/v4.34.1)
 [![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-ready--to--code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/leanprover-community/physlib)
 [![Ask DeepWiki](https://deepwiki.com/badge.svg)](https://deepwiki.com/leanprover-community/physlib)
 [![api_docs](https://img.shields.io/badge/doc-API_docs-blue)](https://physlib.io/docs/)