diff --git a/lake-manifest.json b/lake-manifest.json
index 0ec4bf49..bb1980fe 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "958ad8be87e9d49c497c6ce589c93d3dbcbd6fe2",
+   "rev": "b0be57cc5ec46a829c6afaf7b9c5c5d61b8dbffb",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "61c44bec841faabd47d11c2eda15f57ec2ffe9d5",
+   "rev": "240eddc1bb31420fbbc57fe5cc579435c2522493",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
+   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "140dc642f4f29944abcdcd3096e8ea9b4469c873",
+   "rev": "dba7fbc707774d1ba830fd44d7f92a717e9bf57f",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,17 +55,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "96c67159f161fb6bf6ce91a2587232034ac33d7e",
+   "rev": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.67",
+   "inputRev": "v0.0.71",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a62ecd0343a2dcfbcac6d1e8243f5821879c0244",
+   "rev": "3b779e9d1c73837a3764d516d81f942de391b6f0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "867d9dc77534341321179c9aa40fceda675c50d4",
+   "rev": "f85ad59c9b60647ef736719c23edd4578f723806",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3cabaef23886b82ba46f07018f2786d9496477d6",
+   "rev": "a67fc66cd1ebc0855dc064a4be727798771c0f89",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "e22ed0883c7d7f9a7e294782b6b137b783715386",
+   "rev": "cacb481a1eaa4d7d4530a27b606c60923da21caf",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lean-toolchain b/lean-toolchain
index 28f76d10..27770b57 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.22.0-rc3
\ No newline at end of file
+leanprover/lean4:v4.23.0-rc2
\ No newline at end of file