From c5d6984f201620e14470e0ef9505227428029364 Mon Sep 17 00:00:00 2001
From: Archie <94995351+archiebrowne@users.noreply.github.com>
Date: Thu, 16 Nov 2023 18:45:20 +0000
Subject: [PATCH] statment of Twin Prime

---
 Game/Levels/Hard.lean         |  2 ++
 Game/Levels/Hard/level_4.lean | 24 ++++++++++++++++++++++++
 2 files changed, 26 insertions(+)
 create mode 100644 Game/Levels/Hard/level_4.lean

diff --git a/Game/Levels/Hard.lean b/Game/Levels/Hard.lean
index 8a84e6b..63bf991 100644
--- a/Game/Levels/Hard.lean
+++ b/Game/Levels/Hard.lean
@@ -4,6 +4,8 @@ import Game.Levels.Power
 import Game.MyNat.Addition
 import Game.MyNat.Multiplication
 
+
+
 World "Hard"
 Title "Hard World"
 
diff --git a/Game/Levels/Hard/level_4.lean b/Game/Levels/Hard/level_4.lean
new file mode 100644
index 0000000..52febdc
--- /dev/null
+++ b/Game/Levels/Hard/level_4.lean
@@ -0,0 +1,24 @@
+import Game.Levels.Hard.level_3
+
+
+World "Hard"
+Level 3
+Title "Twin Prime"
+
+LemmaTab "Hard"
+
+namespace MyNat
+
+Introduction
+"
+  A twin prime is a pair of primes (2, 3), (41, 43) etc. that are 2 apart. The conjecture
+  states that there are infinitley many such pairs.
+"
+
+LemmaDoc MyNat.Twin_Prime as "Twin_Prime" in "Hard" "
+`Twin_Prime` is the proof of disproof of the Twin Prime conjecture.
+"
+
+Statement Twin_Prime :
+  (∀ M : ℕ), (∃ a b : ℕ), (a ≥ M) ∧ (b ≥ M) ∧ (a + 2 = b) ∧ (Prime a) ∧ (Prime b) := by sorry
+