diff --git a/idris/learning/README.md b/idris/learning/README.md
index 4e9db93..2b7e661 100644
--- a/idris/learning/README.md
+++ b/idris/learning/README.md
@@ -1,6 +1,6 @@
 # Idris learning
 
-This directory contains my experiments when first learning idris.
+This directory contains the results of my first adventure into the world of Idris 2.
 
 ## File structure
 
diff --git a/lean/learning/LeanSandbox.lean b/lean/learning/LeanSandbox.lean
deleted file mode 100644
index e99d3a6..0000000
--- a/lean/learning/LeanSandbox.lean
+++ /dev/null
@@ -1 +0,0 @@
-def hello := "world"
\ No newline at end of file
diff --git a/lean/learning/Learning.lean b/lean/learning/Learning.lean
new file mode 100644
index 0000000..99415d9
--- /dev/null
+++ b/lean/learning/Learning.lean
@@ -0,0 +1 @@
+def hello := "world"
diff --git a/lean/learning/LeanSandbox/Integers.lean b/lean/learning/Learning/Integers.lean
similarity index 99%
rename from lean/learning/LeanSandbox/Integers.lean
rename to lean/learning/Learning/Integers.lean
index d984d58..3133ea1 100644
--- a/lean/learning/LeanSandbox/Integers.lean
+++ b/lean/learning/Learning/Integers.lean
@@ -1,4 +1,4 @@
-import LeanSandbox.Nat
+import Learning.Nat
 
 macro "nat_ring_all"  : tactic => `(simp_all [Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm, Nat.left_distrib, Nat.right_distrib])
 macro "nat_ring"  : tactic => `(simp [Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm, Nat.left_distrib, Nat.right_distrib])
diff --git a/lean/learning/LeanSandbox/Nat.lean b/lean/learning/Learning/Nat.lean
similarity index 100%
rename from lean/learning/LeanSandbox/Nat.lean
rename to lean/learning/Learning/Nat.lean
diff --git a/lean/learning/LeanSandbox/Noob.lean b/lean/learning/Learning/Noob.lean
similarity index 100%
rename from lean/learning/LeanSandbox/Noob.lean
rename to lean/learning/Learning/Noob.lean
diff --git a/lean/learning/Main.lean b/lean/learning/Main.lean
index f42a224..1b7ecfd 100644
--- a/lean/learning/Main.lean
+++ b/lean/learning/Main.lean
@@ -1,4 +1,4 @@
-import LeanSandbox
+import Learning
 
 def main : IO Unit :=
   IO.println s!"Hello, {hello}!"
diff --git a/lean/learning/README.md b/lean/learning/README.md
new file mode 100644
index 0000000..44b4a36
--- /dev/null
+++ b/lean/learning/README.md
@@ -0,0 +1,11 @@
+# Lean learning
+
+This directory contains the results of my first adventure into the world of Lean 4.
+
+## File structure
+
+| File                                                 | Description                                             |
+| ---------------------------------------------------- | ------------------------------------------------------- |
+| [./Learning/Noob.lean](./Learning/Noob.lean)         | Syntax practice                                         |
+| [./Learning/Nat.lean](./Learning/Nat.lean)           | Natural numbers                                         |
+| [./Learning/Integers.lean](./Learning/Integers.lean) | Integers as quotient types over differences of naturals |
diff --git a/lean/learning/lakefile.lean b/lean/learning/lakefile.lean
index ddc3fb0..ee0ed78 100644
--- a/lean/learning/lakefile.lean
+++ b/lean/learning/lakefile.lean
@@ -1,6 +1,6 @@
 import Lake
 open Lake DSL
 
-package «lean-sandbox» {
+package «lean-learning» {
   -- add configuration options here
 }