diff --git a/server/testgame/TestGame.lean b/server/testgame/TestGame.lean
index efe6e43..e64f995 100644
--- a/server/testgame/TestGame.lean
+++ b/server/testgame/TestGame.lean
@@ -5,8 +5,7 @@ import TestGame.Levels.Implication
 import TestGame.Levels.Predicate
 import TestGame.Levels.Contradiction
 import TestGame.Levels.Prime
-
-import TestGame.Levels.Naturals.L31_Sum
+import TestGame.Levels.Induction
 
 Game "TestGame"
 
@@ -65,4 +64,4 @@ Conclusion
 
 Path Proposition → Implication → Predicate → Contradiction
 Path Predicate → Prime
-Path Predicate → Nat2
+Path Predicate → Induction
diff --git a/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean b/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean
index 8bd514a..5c350b9 100644
--- a/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean
+++ b/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean
@@ -47,18 +47,19 @@ Message (A : Prop) (B : Prop) (h : A → ¬ B) (g : A ∧ B) : False =>
 "
 
 Message (A : Prop) (B : Prop) (h : A → ¬ B) (g : A) (f : B) : False =>
-" Auf Deutsch: \"Als Zwischenresultat haben wir `¬ B`.\"
+"
+Auf Deutsch: \"Als Zwischenresultat haben wir `¬ B`.\"
 
-  In Lean :
+In Lean :
 
-  ```
-  have k : ¬ B
-  [Beweis von k]
-  ```
+```
+have k : ¬ B
+[Beweis von k]
+```
 "
 
-example (n : ℕ) : n.succ + 2 = n + 3 := by
-ring_nf
+-- example (n : ℕ) : n.succ + 2 = n + 3 := by
+-- ring_nf
 
 Conclusion ""
 
diff --git a/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean b/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean
index f070cae..bc7f5db 100644
--- a/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean
+++ b/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean
@@ -7,7 +7,7 @@ import Mathlib.Tactic.Ring
 import TestGame.ToBePorted
 
 Game "TestGame"
-World "Proving"
+World "Contradiction"
 Level 6
 
 Title "Contradiction"
diff --git a/server/testgame/TestGame/Levels/Induction.lean b/server/testgame/TestGame/Levels/Induction.lean
new file mode 100644
index 0000000..1c320f2
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Induction.lean
@@ -0,0 +1,2 @@
+import TestGame.Levels.Induction.L31_Sum
+import TestGame.Levels.Induction.L32_Induction
diff --git a/server/testgame/TestGame/Levels/Naturals/L31_Sum.lean b/server/testgame/TestGame/Levels/Induction/L31_Sum.lean
similarity index 83%
rename from server/testgame/TestGame/Levels/Naturals/L31_Sum.lean
rename to server/testgame/TestGame/Levels/Induction/L31_Sum.lean
index aaf51f0..eca12b2 100644
--- a/server/testgame/TestGame/Levels/Naturals/L31_Sum.lean
+++ b/server/testgame/TestGame/Levels/Induction/L31_Sum.lean
@@ -6,7 +6,7 @@ import TestGame.Metadata
 set_option tactic.hygienic false
 
 Game "TestGame"
-World "Nat2"
+World "Induction"
 Level 1
 
 Title "Summe"
@@ -16,7 +16,7 @@ Introduction
 "
 
 Statement
-"Zeige $\\sum_{i=0}^{n} i = \\frac{n \\cdot {n+1}}{2}$"
+""
     (n : ℕ) : 2 * (∑ i : Fin (n+1), ↑i) = n * (n + 1) := by
   induction' n with n hn
   simp
diff --git a/server/testgame/TestGame/Levels/Induction/L32_Induction.lean b/server/testgame/TestGame/Levels/Induction/L32_Induction.lean
new file mode 100644
index 0000000..4f6aa2e
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Induction/L32_Induction.lean
@@ -0,0 +1,37 @@
+import TestGame.Metadata
+import Mathlib.Tactic.Ring
+import Mathlib
+
+Game "TestGame"
+World "Induction"
+Level 2
+
+Title "Induktion"
+
+Introduction
+"
+TODO: Induktion (& induktion vs rcases)
+
+"
+
+
+theorem nat_succ (n : ℕ) : Nat.succ n = n + 1 := rfl
+
+lemma hh1 (n m : ℕ) (h : 2 * m = n) : m = n / 2 := by
+  rw [←h]
+  rw [Nat.mul_div_right]
+  simp
+
+Statement
+"Zeige $\\sum_{i = 0}^n i = \\frac{n ⬝ (n + 1)}{2}$."
+  (n : ℕ) : (∑ i : Fin (n + 1), ↑i) = n * (n + 1) / 2 := by
+  apply hh1
+  induction' n with n hn
+  simp
+  sorry
+  -- rw [Fin.sum_univ_castSucc]
+  -- simp [nat_succ]
+  -- rw [mul_add, hn]
+  -- ring
+
+Tactics ring
diff --git a/server/testgame/TestGame/Levels/Naturals/L33_Prime.lean b/server/testgame/TestGame/Levels/LeftOvers/L33_Prime.lean
similarity index 100%
rename from server/testgame/TestGame/Levels/Naturals/L33_Prime.lean
rename to server/testgame/TestGame/Levels/LeftOvers/L33_Prime.lean
diff --git a/server/testgame/TestGame/Levels/Naturals/L34_ExistsUnique.lean b/server/testgame/TestGame/Levels/LeftOvers/L34_ExistsUnique.lean
similarity index 100%
rename from server/testgame/TestGame/Levels/Naturals/L34_ExistsUnique.lean
rename to server/testgame/TestGame/Levels/LeftOvers/L34_ExistsUnique.lean
diff --git a/server/testgame/TestGame/Levels/Naturals/Lxx_Prime.lean b/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean
similarity index 100%
rename from server/testgame/TestGame/Levels/Naturals/Lxx_Prime.lean
rename to server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean
diff --git a/server/testgame/TestGame/Levels/Naturals/L32_Induction.lean b/server/testgame/TestGame/Levels/Naturals/L32_Induction.lean
deleted file mode 100644
index 2e4ce58..0000000
--- a/server/testgame/TestGame/Levels/Naturals/L32_Induction.lean
+++ /dev/null
@@ -1,23 +0,0 @@
-import TestGame.Metadata
-import Mathlib.Tactic.Ring
-
-Game "TestGame"
-World "Nat2"
-Level 2
-
-Title "Induktion"
-
-Introduction
-"
-TODO: Induktion (& induktion vs rcases)
-
-"
-
-Statement "" : True := by
-  trivial
-
-Conclusion
-"
-"
-
-Tactics ring