diff --git a/QuerySMTTests.lean b/QuerySMTTests.lean
new file mode 100644
index 0000000..066878e
--- /dev/null
+++ b/QuerySMTTests.lean
@@ -0,0 +1,3 @@
+import QuerySMTTests.Issues
+import QuerySMTTests.Tests
+import QuerySMTTests.Tests2
diff --git a/QuerySMT/issues.lean b/QuerySMTTests/Issues.lean
similarity index 100%
rename from QuerySMT/issues.lean
rename to QuerySMTTests/Issues.lean
diff --git a/QuerySMT/tests.lean b/QuerySMTTests/Tests.lean
similarity index 100%
rename from QuerySMT/tests.lean
rename to QuerySMTTests/Tests.lean
diff --git a/QuerySMT/tests2.lean b/QuerySMTTests/Tests2.lean
similarity index 100%
rename from QuerySMT/tests2.lean
rename to QuerySMTTests/Tests2.lean
diff --git a/lakefile.lean b/lakefile.lean
deleted file mode 100644
index 2ae3e43..0000000
--- a/lakefile.lean
+++ /dev/null
@@ -1,16 +0,0 @@
-import Lake
-open Lake DSL
-
-require «mathlib» from git "https://github.com/leanprover-community/mathlib4" @ "v4.29.0"
-
-require «Duper» from git "https://github.com/leanprover-community/duper.git" @ "a05206eadfece7682abf44d52e8fd8c7110ef58a"
-
-require «premise-selection» from git "https://github.com/hanwenzhu/premise-selection" @ "v4.29.0"
-
-package QuerySMT {
-  precompileModules := false
-  preferReleaseBuild := false
-}
-
-@[default_target]
-lean_lib QuerySMT
diff --git a/lakefile.toml b/lakefile.toml
new file mode 100644
index 0000000..6e51f45
--- /dev/null
+++ b/lakefile.toml
@@ -0,0 +1,26 @@
+name = "QuerySMT"
+version = "0.1.0"
+defaultTargets = ["QuerySMT"]
+precompileModules = false
+preferReleaseBuild = false
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4"
+rev = "v4.29.0"
+
+[[require]]
+name = "Duper"
+git = "https://github.com/leanprover-community/duper.git"
+rev = "a05206eadfece7682abf44d52e8fd8c7110ef58a"
+
+[[require]]
+name = "premise-selection"
+git = "https://github.com/hanwenzhu/premise-selection"
+rev = "v4.29.0"
+
+[[lean_lib]]
+name = "QuerySMT"
+
+[[lean_lib]]
+name = "QuerySMTTests"