diff --git a/lake-manifest.json b/lake-manifest.json
index 8a989b9b..c8cbde9e 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0df2e3c2047ada0d7a2e33dbc6ba2788a44a6062",
+   "rev": "c98ae54af00eaefe79c51b2b278361ca94e59bfb",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,10 +55,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "135329b50b116dcc2c021c318c365e82a048856f",
+   "rev": "45777338ffb69576c945dfe9466665b8023a8b8c",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.80",
+   "inputRev": "v0.0.80+lean-v4.25.2",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
diff --git a/lean-toolchain b/lean-toolchain
index 96c38be8..7a22c3f3 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.25.1
\ No newline at end of file
+leanprover/lean4:v4.25.2
\ No newline at end of file
diff --git a/scripts/build_docs.sh b/scripts/build_docs.sh
index 0d1347b2..97acba98 100755
--- a/scripts/build_docs.sh
+++ b/scripts/build_docs.sh
@@ -22,7 +22,7 @@ path = "../"
 [[require]]
 scope = "leanprover"
 name = "doc-gen4"
-rev = "TOOLCHAIN"
+rev = "v4.25.1"
 EOF
 }
 
@@ -33,7 +33,8 @@ mkdir -p docbuild
 template > docbuild/lakefile.toml
 
 # Substitute the toolchain from lean-toolchain into docbuild/lakefile.toml
-sed -i s/TOOLCHAIN/`grep -oP 'v4\..*' lean-toolchain`/ docbuild/lakefile.toml
+# Temporarily disabled for 4.25.2.
+# sed -i s/TOOLCHAIN/`grep -oP 'v4\..*' lean-toolchain`/ docbuild/lakefile.toml
 
 # Initialise docbuild as a Lean project
 cd docbuild