From e73913e8844a67b099c83adfb5dcfc99671acf3d Mon Sep 17 00:00:00 2001
From: Archie <94995351+archiebrowne@users.noreply.github.com>
Date: Thu, 16 Nov 2023 19:25:47 +0000
Subject: [PATCH] twin prime

---
 Game/Levels/Hard.lean         | 2 ++
 Game/Levels/Hard/level_2.lean | 3 +--
 Game/Levels/Hard/level_3.lean | 4 ++--
 Game/Levels/Hard/level_4.lean | 3 +--
 4 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/Game/Levels/Hard.lean b/Game/Levels/Hard.lean
index 63bf991..101d8d3 100644
--- a/Game/Levels/Hard.lean
+++ b/Game/Levels/Hard.lean
@@ -3,6 +3,8 @@ import Game.Levels.LessOrEqual
 import Game.Levels.Power
 import Game.MyNat.Addition
 import Game.MyNat.Multiplication
+import Game.MyNat.Prime
+
 
 
 
diff --git a/Game/Levels/Hard/level_2.lean b/Game/Levels/Hard/level_2.lean
index 4ade16b..d176fe3 100644
--- a/Game/Levels/Hard/level_2.lean
+++ b/Game/Levels/Hard/level_2.lean
@@ -1,7 +1,6 @@
 import Game.Levels.Hard.level_1
 
 
-
 World "Hard"
 Level 2
 Title "Collatz"
@@ -20,7 +19,7 @@ Introduction
 "
 
 LemmaDoc MyNat.Colatz as "Collatz" in "Hard" "
-`Collatz` is the proof of disproof of the Collatz conjecture.
+`Collatz` is the proof of the Collatz conjecture.
 "
 
 -- halving used for the sequence
diff --git a/Game/Levels/Hard/level_3.lean b/Game/Levels/Hard/level_3.lean
index d62161a..36c171f 100644
--- a/Game/Levels/Hard/level_3.lean
+++ b/Game/Levels/Hard/level_3.lean
@@ -17,8 +17,8 @@ Introduction
 "
 
 LemmaDoc MyNat.Golbach as "Golbach" in "Hard" "
-`Golbach` is the proof of disproof of the Golbach conjecture.
+`Golbach` is the proof of the Golbach conjecture.
 "
 
-Statement Golbach : (∀ n : ℕ), n ≥ 2 → (∃ a b : ℕ), (Prime a) ∧ (Prime b) ∧ (n = a + b) := by
+Statement Golbach : ∀ (n : ℕ), n ≥ 2 → ∃ (a b : ℕ), (Prime a) ∧ (Prime b) ∧ (n = a + b) := by
   sorry
diff --git a/Game/Levels/Hard/level_4.lean b/Game/Levels/Hard/level_4.lean
index 52febdc..03e24e8 100644
--- a/Game/Levels/Hard/level_4.lean
+++ b/Game/Levels/Hard/level_4.lean
@@ -16,9 +16,8 @@ Introduction
 "
 
 LemmaDoc MyNat.Twin_Prime as "Twin_Prime" in "Hard" "
-`Twin_Prime` is the proof of disproof of the Twin Prime conjecture.
+`Twin_Prime` is the proof of the Twin Prime conjecture.
 "
 
 Statement Twin_Prime :
   (∀ M : ℕ), (∃ a b : ℕ), (a ≥ M) ∧ (b ≥ M) ∧ (a + 2 = b) ∧ (Prime a) ∧ (Prime b) := by sorry
-