diff --git a/lakefile.toml b/lakefile.toml
new file mode 100644
index 0000000..589e047
--- /dev/null
+++ b/lakefile.toml
@@ -0,0 +1,10 @@
+name = "REPL"
+defaultTargets = ["repl"]
+
+[[lean_lib]]
+name = "REPL"
+
+[[lean_exe]]
+name = "repl"
+root = "REPL.Main"
+supportInterpreter = true
diff --git a/test/Mathlib/lakefile.toml b/test/Mathlib/lakefile.toml
new file mode 100644
index 0000000..1546899
--- /dev/null
+++ b/test/Mathlib/lakefile.toml
@@ -0,0 +1,11 @@
+name = "«repl-mathlib-tests»"
+defaultTargets = ["ReplMathlibTests"]
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4"
+rev = "master"
+
+[[lean_lib]]
+name = "ReplMathlibTests"
+globs = ["test.+"]