Golbach Conjecture

leanprover-community · Nov 16, 2023 · 67c7253 · 67c7253
1 parent 3ee7a21
commit 67c7253
Show file tree

Hide file tree

Showing 2 changed files with 24 additions and 2 deletions.
diff --git 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
@@ -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
Original file line number	Diff line number	Diff line change
		@@ -1,6 +1,4 @@
		import Game.Levels.Hard.level_1
		import Game.MyNat.Multiplication




Expand Down