diff --git a/.gitignore b/.gitignore
index 1cb9f3c..20c60d7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,2 @@
-*.olean
-/_target
-/leanpkg.path
+/build
+/lake-packages/*
diff --git a/Bookshelf.lean b/Bookshelf.lean
new file mode 100644
index 0000000..e99d3a6
--- /dev/null
+++ b/Bookshelf.lean
@@ -0,0 +1 @@
+def hello := "world"
\ No newline at end of file
diff --git a/Main.lean b/Main.lean
new file mode 100644
index 0000000..e60cc2b
--- /dev/null
+++ b/Main.lean
@@ -0,0 +1,4 @@
+import «Bookshelf»
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"
diff --git a/lakefile.lean b/lakefile.lean
new file mode 100644
index 0000000..86589d0
--- /dev/null
+++ b/lakefile.lean
@@ -0,0 +1,15 @@
+import Lake
+open Lake DSL
+
+package «bookshelf» {
+  -- add package configuration options here
+}
+
+lean_lib «Bookshelf» {
+  -- add library configuration options here
+}
+
+@[default_target]
+lean_exe «bookshelf» {
+  root := `Main
+}
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..5bf01da
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-02-10
diff --git a/leanpkg.toml b/leanpkg.toml
deleted file mode 100644
index 17b4e4c..0000000
--- a/leanpkg.toml
+++ /dev/null
@@ -1,8 +0,0 @@
-[package]
-name = "bookshelf"
-version = "0.1"
-lean_version = "leanprover-community/lean:3.50.3"
-path = "src"
-
-[dependencies]
-mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "4c19a16e4b705bf135cf9a80ac18fcc99c438514"}