diff --git a/README.md b/README.md
index 2e37d59..aab9e0a 100644
--- a/README.md
+++ b/README.md
@@ -51,7 +51,7 @@ The template repository is organized as follows (listing the main folders and fi
 and environment.
 - [`CONTRIBUTING.md`](CONTRIBUTING.md) should provide the guidelines for contributing to the
 project.
-- [`lakefile.lean`](lakefile.lean) is the configuration file for the Lake build system used in
+- [`lakefile.toml`](lakefile.toml) is the configuration file for the Lake build system used in
 Lean projects.
 - [`lean-toolchain`](lean-toolchain) specifies the Lean version and toolchain used for the project.
 
@@ -65,7 +65,7 @@ project name.
 - [`Project/Example.lean`](Project/Example.lean): Remove it and replace it with your actual
 project code.
 - [`CONTRIBUTING.md`](CONTRIBUTING.md): Customise the guidelines for contributing to the project.
-- [`lakefile.lean`](lakefile.lean): Find and replace `Project` with your actual project name.
+- [`lakefile.toml`](lakefile.toml): Find and replace `Project` with your actual project name.
 - [`Project.lean`](Project.lean): Rename the main file and the imports
 to match your actual project name.
 
diff --git a/lakefile.lean b/lakefile.lean
deleted file mode 100644
index 382d63c..0000000
--- a/lakefile.lean
+++ /dev/null
@@ -1,21 +0,0 @@
-import Lake
-open Lake DSL
-
-/- Define the package configuration for the project.
-Includes options for Lean's pretty-printer and implicit argument settings. -/
-package «Project» where
-  leanOptions := #[
-    ⟨`pp.unicode.fun, true⟩,      -- Pretty-print `fun a ↦ b`
-    ⟨`autoImplicit, false⟩,       -- Disable auto-implicit arguments
-    ⟨`relaxedAutoImplicit, false⟩ -- Disable relaxed auto-implicit arguments
-  ]
-
-/- Specify external dependencies required for this project. -/
-require mathlib from git "https://github.com/leanprover-community/mathlib4.git"
-
-/- Define the default Lean library target for the project.
-This can be customized with additional library configuration options.
--/
-@[default_target]
-lean_lib «Project» where
-  -- Add any library configuration options here
diff --git a/lakefile.toml b/lakefile.toml
new file mode 100644
index 0000000..281da52
--- /dev/null
+++ b/lakefile.toml
@@ -0,0 +1,14 @@
+name = "Project"
+defaultTargets = ["Project"]
+
+[leanOptions]
+pp.unicode.fun = true
+autoImplicit = false
+relaxedAutoImplicit = false
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4.git"
+
+[[lean_lib]]
+name = "Project"