statment of Twin Prime

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

Hide file tree

Showing 2 changed files with 26 additions and 0 deletions.
diff --git 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
@@ -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
+