diff --git a/HammerCore/lake-manifest.json b/HammerCore/lake-manifest.json
index d7819e3..70fd032 100644
--- a/HammerCore/lake-manifest.json
+++ b/HammerCore/lake-manifest.json
@@ -5,40 +5,40 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "93e949f61679a9546d543a604f3f88b2a5eef262",
+   "rev": "03488acde08efdb914d9cacaf72618fd39c66701",
    "name": "Duper",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.26.0",
+   "inputRev": "v4.27.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2f6d238744c4cb07fdc91240feaf5d4221a27931",
+   "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.26.0",
+   "inputRev": "v4.27.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3",
+   "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.26.0",
+   "inputRev": "v4.27.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/lean-auto.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6e66058117f0d073914c2c1f674b880537d9eb2e",
+   "rev": "7e8f3ab431d4790bd803e467d661b1be2522bfd3",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.26.0-hammer",
+   "inputRev": "v4.27.0-hammer",
    "inherited": true,
    "configFile": "lakefile.lean"}],
  "name": "HammerCore",
diff --git a/HammerCore/lakefile.lean b/HammerCore/lakefile.lean
index 73e73c1..278d08a 100644
--- a/HammerCore/lakefile.lean
+++ b/HammerCore/lakefile.lean
@@ -1,9 +1,9 @@
 import Lake
 open Lake DSL
 
-require «aesop» from git "https://github.com/leanprover-community/aesop" @ "v4.26.0"
+require «aesop» from git "https://github.com/leanprover-community/aesop" @ "v4.27.0"
 
-require «Duper» from git "https://github.com/leanprover-community/duper.git" @ "v4.26.0"
+require «Duper» from git "https://github.com/leanprover-community/duper.git" @ "v4.27.0"
 
 package HammerCore {
   precompileModules := true
diff --git a/HammerCore/lean-toolchain b/HammerCore/lean-toolchain
index e59446d..5249182 100644
--- a/HammerCore/lean-toolchain
+++ b/HammerCore/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.26.0
+leanprover/lean4:v4.27.0
diff --git a/README.md b/README.md
index 76dd95c..64d6017 100644
--- a/README.md
+++ b/README.md
@@ -2,36 +2,38 @@
 
 LeanHammer is an automated reasoning tool for Lean that brings together multiple proof search and reconstruction techniques and combines them into one tool. The `hammer` tactic provided by LeanHammer uses a variety of techniques to search for a proof of the current goal, then constructs a suggestion for a tactic script which can replace the `hammer` invocation.
 
-LeanHammer is in an early stage of its development and is therefore subject to breaking changes. There are currently versions of the hammer that are compatible with the stable versions of Lean from `v4.20.0` through `v4.26.0` (and the corresponding versions of Mathlib).
+LeanHammer is in an early stage of its development and is therefore subject to breaking changes. There are currently versions of the hammer that are compatible with the stable versions of Lean from `v4.20.0` through `v4.27.0` (and the corresponding versions of Mathlib).
+
+***Note:** Although the LeanHammer repository has been updated to support `v4.27.0`, the LeanPremise server which LeanHammer uses for premise selection is still being updated from `v4.26.0` to `v4.27.0`. During the intermediate period while this update is occurring, premise selection may be slower and less accurate than usual. This note will be removed once the server has been fully updated to `v4.27.0`.*
 
 Pull requests and issues are welcome.
 
 ## Adding LeanHammer to Your Project
 
-To add LeanHammer for v4.26.0 to an existing project with a `lakefile.toml` file, replace the Mathlib dependency in `lakefile.toml` with the following:
+To add LeanHammer for `v4.27.0` to an existing project with a `lakefile.toml` file, replace the Mathlib dependency in `lakefile.toml` with the following:
 
 ```toml
 [[require]]
 name = "Hammer"
 git = "https://github.com/JOSHCLUNE/LeanHammer"
-rev = "v4.26.0"
+rev = "v4.27.0"
 
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "v4.26.0"
+rev = "v4.27.0"
 ```
 The file `lean-toolchain` should contain the following:
 ```
-leanprover/lean4:v4.26.0
+leanprover/lean4:v4.27.0
 ```
 
 If you have a project with a `lakefile.lean` instead of `lakefile.toml`, you can use this instead:
 
 ```lean
-require Hammer from git "https://github.com/JOSHCLUNE/LeanHammer" @ "v4.26.0"
+require Hammer from git "https://github.com/JOSHCLUNE/LeanHammer" @ "v4.27.0"
 
-require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.26.0"
+require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.27.0"
 ```
 
 Then use `lake update` to fetch the hammer and the corresponding versions of Lean and Mathlib. This also retrieves the Zipperposition executable that comes with LeanHammer. (This executable will be stored in the existing project's `.lake` directory.) The following example should then compile without any warnings or errors:
diff --git a/lake-manifest.json b/lake-manifest.json
index 74d04f6..0d04ea4 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -12,60 +12,60 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9312503909aa8e8bb392530145cc1677a6298574",
+   "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.26.0",
+   "inputRev": "v4.27.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/hanwenzhu/premise-selection",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d648fd5130a972d609ef846c0fa3e853753638bf",
+   "rev": "d0f19843efc9f3632325bc5eb45b1e924959dc00",
    "name": "«premise-selection»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.26.0",
+   "inputRev": "v4.27.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/duper.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "93e949f61679a9546d543a604f3f88b2a5eef262",
+   "rev": "03488acde08efdb914d9cacaf72618fd39c66701",
    "name": "Duper",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.26.0",
+   "inputRev": "v4.27.0",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2f6d238744c4cb07fdc91240feaf5d4221a27931",
+   "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.26.0",
+   "inputRev": "v4.27.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3",
+   "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.26.0",
+   "inputRev": "v4.27.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/lean-auto.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6e66058117f0d073914c2c1f674b880537d9eb2e",
+   "rev": "7e8f3ab431d4790bd803e467d661b1be2522bfd3",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.26.0-hammer",
+   "inputRev": "v4.27.0-hammer",
    "inherited": true,
    "configFile": "lakefile.lean"}],
  "name": "Hammer",
diff --git a/lakefile.toml b/lakefile.toml
index 6d74bb6..e947900 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -6,12 +6,12 @@ defaultTargets = ["Hammer"]
 [[require]]
 name = "«premise-selection»"
 git = "https://github.com/hanwenzhu/premise-selection"
-rev = "v4.26.0"
+rev = "v4.27.0"
 
 [[require]]
 name = "Qq"
 git = "https://github.com/leanprover-community/quote4.git"
-rev = "v4.26.0"
+rev = "v4.27.0"
 
 [[require]]
 name = "HammerCore"
diff --git a/lean-toolchain b/lean-toolchain
index e59446d..5249182 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.26.0
+leanprover/lean4:v4.27.0