Update Thu Sep 19 20:34:58 EDT 2024

Author: hrmacbeth

Math2001/Homework/hw3.lean

@@ -21,7 +21,7 @@ theorem problem2 {t : ℚ} (h : t ^ 2 + t - 6 = 0) : t = 2 ∨ t = -3 := by
   sorry
 
 @[autograded 3]
-example : ∃ a b : ℕ, a ≠ 0 ∧ 2 ^ a = 5 * b + 1 := by
+theorem problem3 : ∃ a b : ℕ, a ≠ 0 ∧ 2 ^ a = 5 * b + 1 := by
   sorry
 
 @[autograded 5]