twin prime

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

Hide file tree

Showing 4 changed files with 6 additions and 6 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
-