diff --git a/lakefile.lean b/lakefile.lean
deleted file mode 100644
index 2a69fad..0000000
--- a/lakefile.lean
+++ /dev/null
@@ -1,16 +0,0 @@
-import Lake
-open Lake DSL
-
-require «premise-selection» from git "https://github.com/hanwenzhu/premise-selection" @ "v4.26.0"
-
-require «Qq» from git "https://github.com/leanprover-community/quote4.git" @ "v4.26.0"
-
-require «HammerCore» from "./HammerCore"
-
-package Hammer {
-  precompileModules := true
-  preferReleaseBuild := true
-}
-
-@[default_target]
-lean_lib Hammer
diff --git a/lakefile.toml b/lakefile.toml
new file mode 100644
index 0000000..6d74bb6
--- /dev/null
+++ b/lakefile.toml
@@ -0,0 +1,21 @@
+name = "Hammer"
+precompileModules = true
+preferReleaseBuild = true
+defaultTargets = ["Hammer"]
+
+[[require]]
+name = "«premise-selection»"
+git = "https://github.com/hanwenzhu/premise-selection"
+rev = "v4.26.0"
+
+[[require]]
+name = "Qq"
+git = "https://github.com/leanprover-community/quote4.git"
+rev = "v4.26.0"
+
+[[require]]
+name = "HammerCore"
+path = "./HammerCore"
+
+[[lean_lib]]
+name = "Hammer"