From 67c72539e83a08edbd1f7ffeaa62d4fef6d7528e Mon Sep 17 00:00:00 2001
From: Archie <94995351+archiebrowne@users.noreply.github.com>
Date: Thu, 16 Nov 2023 18:35:03 +0000
Subject: [PATCH] Golbach Conjecture

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

diff --git a/Game/Levels/Hard/level_2.lean b/Game/Levels/Hard/level_2.lean
index a5cb780..4ade16b 100644
--- a/Game/Levels/Hard/level_2.lean
+++ b/Game/Levels/Hard/level_2.lean
@@ -1,6 +1,4 @@
 import Game.Levels.Hard.level_1
-import Game.MyNat.Multiplication
-
 
 
 
diff --git a/Game/Levels/Hard/level_3.lean b/Game/Levels/Hard/level_3.lean
new file mode 100644
index 0000000..d62161a
--- /dev/null
+++ b/Game/Levels/Hard/level_3.lean
@@ -0,0 +1,24 @@
+import Game.Levels.Hard.level_2
+
+
+World "Hard"
+Level 3
+Title "Golbach"
+
+LemmaTab "Hard"
+
+namespace MyNat
+
+Introduction
+"
+  The Golbach conjecture, first posed in 1792 in a letter to Euler states that every
+  natural number greater than 2 is the sum of two prime numbers. It remains unproven
+  to this day, but has been checked for all naturals up to 4 x 10¹⁸.
+"
+
+LemmaDoc MyNat.Golbach as "Golbach" in "Hard" "
+`Golbach` is the proof of disproof of the Golbach conjecture.
+"
+
+Statement Golbach : (∀ n : ℕ), n ≥ 2 → (∃ a b : ℕ), (Prime a) ∧ (Prime b) ∧ (n = a + b) := by
+  sorry