diff --git a/Math2001/Homework/hw1.lean b/Math2001/Homework/hw1.lean
deleted file mode 100644
index 50d321f5..00000000
--- a/Math2001/Homework/hw1.lean
+++ /dev/null
@@ -1,33 +0,0 @@
-/- Copyright (c) Heather Macbeth, 2023.  All rights reserved. -/
-import Mathlib.Data.Real.Basic
-import Library.Basic
-import AutograderLib
-
-math2001_init
-
-/-! # Homework 1
-
-Don't forget to compare with the text version,
-https://github.com/hrmacbeth/math2001/wiki/Homework-1,
-for clearer statements and any special instructions. -/
-
-
-@[autograded 5]
-theorem problem1 {p q : ℤ} (h1 : p + 4 * q = 1) (h2 : q - 1 = 2) : p = -11 := by
-  sorry
-
-@[autograded 5]
-theorem problem2 {a b : ℝ} (h1 : a + 2 * b = 4) (h2 : a - b = 1) : a = 2 := by
-  sorry
-
-@[autograded 5]
-theorem problem3 {x : ℤ} (hx : x ≥ 9) : x ^ 3 - 8 * x ^ 2 + 2 * x ≥ 3 := by
-  sorry
-
-@[autograded 5]
-theorem problem4 {x : ℚ} : x ^ 2 - 2 * x ≥ -1 := by
-  sorry
-
-@[autograded 5]
-theorem problem5 (a b : ℝ) (h1 : -b ≤ a) (h2 : a ≤ b) : a ^ 2 ≤ b ^ 2 := by
-  sorry
diff --git a/Math2001/Homework/hw10.lean b/Math2001/Homework/hw10.lean
deleted file mode 100644
index 2a6c998e..00000000
--- a/Math2001/Homework/hw10.lean
+++ /dev/null
@@ -1,122 +0,0 @@
-/- Copyright (c) Heather Macbeth, 2023-4.  All rights reserved. -/
-import Mathlib.Data.Real.Basic
-import Library.Basic
-import Library.Tactic.ModEq
-import AutograderLib
-
-math2001_init
-set_option quotPrecheck false
-
-
-/-! # Homework 10
-
-Don't forget to compare with the text version,
-https://github.com/hrmacbeth/math2001/wiki/Homework-10,
-for clearer statements and any special instructions. -/
-
-
-@[autograded 4]
-theorem problem1a : { m : ℤ | m ≥ 10 } ⊆ { n : ℤ | n ^ 3 - 8 * n ^ 2 ≥ 2 * n } := by
-  sorry
-
-@[autograded 4]
-theorem problem1b : { m : ℤ | m ≥ 10 } ⊈ { n : ℤ | n ^ 3 - 8 * n ^ 2 ≥ 2 * n } := by
-  sorry
-
-
-@[autograded 4]
-theorem problem2a : { t : ℝ | t ^ 2 - 5 * t + 6 = 0 } = { s : ℝ | s = 2 } := by
-  sorry
-
-@[autograded 4]
-theorem problem2b : { t : ℝ | t ^ 2 - 5 * t + 6 = 0 } ≠ { s : ℝ | s = 2 } := by
-  sorry
-
-
-@[autograded 4]
-theorem problem3a : {1, 2, 3} = {1, 2} := by
-  sorry
-
-@[autograded 4]
-theorem problem3b : {1, 2, 3} ≠ {1, 2} := by
-  sorry
-
-
-@[autograded 4]
-theorem problem4 : { r : ℤ | r ≡ 8 [ZMOD 10] }
-    ⊆ { s : ℤ | s ≡ 0 [ZMOD 2] } ∩ { t : ℤ | t ≡ 3 [ZMOD 5] } := by
-  sorry
-
-
-/-! ### Problem 5 starts here -/
-
-infix:50 "∼" => fun (x y : ℤ) ↦ x + y ≡ 0 [ZMOD 3]
-
-@[autograded 2]
-theorem problem51a : Reflexive (· ∼ ·) := by
-  sorry
-
-@[autograded 2]
-theorem problem51b : ¬ Reflexive (· ∼ ·) := by
-  sorry
-
-@[autograded 2]
-theorem problem52a : Symmetric (· ∼ ·) := by
-  sorry
-
-@[autograded 2]
-theorem problem52b : ¬ Symmetric (· ∼ ·) := by
-  sorry
-
-@[autograded 2]
-theorem problem53a : AntiSymmetric (· ∼ ·) := by
-  sorry
-
-@[autograded 2]
-theorem problem53b : ¬ AntiSymmetric (· ∼ ·) := by
-  sorry
-
-@[autograded 2]
-theorem problem54a : Transitive (· ∼ ·) := by
-  sorry
-
-@[autograded 2]
-theorem problem54b : ¬ Transitive (· ∼ ·) := by
-  sorry
-
-
-/-! ### Problem 6 starts here -/
-
-infix:50 "≺" => fun ((x1, y1) : ℝ × ℝ) (x2, y2) ↦ (x1 ≤ x2 ∧ y1 ≤ y2)
-
-@[autograded 2]
-theorem problem61a : Reflexive (· ≺ ·) := by
-  sorry
-
-@[autograded 2]
-theorem problem61b : ¬ Reflexive (· ≺ ·) := by
-  sorry
-
-@[autograded 2]
-theorem problem62a : Symmetric (· ≺ ·) := by
-  sorry
-
-@[autograded 2]
-theorem problem62b : ¬ Symmetric (· ≺ ·) := by
-  sorry
-
-@[autograded 2]
-theorem problem63a : AntiSymmetric (· ≺ ·) := by
-  sorry
-
-@[autograded 2]
-theorem problem63b : ¬ AntiSymmetric (· ≺ ·) := by
-  sorry
-
-@[autograded 2]
-theorem problem64a : Transitive (· ≺ ·) := by
-  sorry
-
-@[autograded 2]
-theorem problem64b : ¬ Transitive (· ≺ ·) := by
-  sorry
diff --git a/Math2001/Homework/hw2.lean b/Math2001/Homework/hw2.lean
deleted file mode 100644
index 36d3c700..00000000
--- a/Math2001/Homework/hw2.lean
+++ /dev/null
@@ -1,37 +0,0 @@
-/- Copyright (c) Heather Macbeth, 2023.  All rights reserved. -/
-import Mathlib.Data.Real.Basic
-import Library.Basic
-import AutograderLib
-
-math2001_init
-
-/-! # Homework 2
-
-Don't forget to compare with the text version,
-https://github.com/hrmacbeth/math2001/wiki/Homework-2,
-for clearer statements and any special instructions. -/
-
-
-@[autograded 4]
-theorem problem1 {x : ℚ} (h1 : x ^ 2 = 4) (h2 : 1 < x) : x = 2 := by
-  sorry
-
-@[autograded 5]
-theorem problem2 {s : ℚ} (h1 : 3 * s ≤ -6) (h2 : 2 * s ≥ -4) : s = -2 := by
-  sorry
-
-@[autograded 2]
-theorem problem3 {a b : ℝ} (h : a = 2 - b) : a + b = 2 ∨ a + b = 8 := by
-  sorry
-
-@[autograded 4]
-theorem problem4 {t : ℚ} (h : t = -2 ∨ t = 3) : t ^ 2 - t - 6 = 0 := by
-  sorry
-
-@[autograded 5]
-theorem problem5 {x : ℤ} : 2 * x ≠ 7 := by
-  sorry
-
-@[autograded 5]
-theorem problem6 {t : ℝ} (ht : t ^ 3 = t ^ 2) : t = 1 ∨ t = 0 := by
-  sorry
diff --git a/Math2001/Homework/hw3.lean b/Math2001/Homework/hw3.lean
deleted file mode 100644
index 15a2232c..00000000
--- a/Math2001/Homework/hw3.lean
+++ /dev/null
@@ -1,42 +0,0 @@
-/- Copyright (c) Heather Macbeth, 2023.  All rights reserved. -/
-import Library.Basic
-import AutograderLib
-
-math2001_init
-
-open Nat
-
-/-! # Homework 3
-
-Don't forget to compare with the text version,
-https://github.com/hrmacbeth/math2001/wiki/Homework-3,
-for clearer statements and any special instructions. -/
-
-
-@[autograded 3]
-theorem problem1 : ∃ x : ℚ, x < 0 ∧ x ^ 2 < 1 := by
-  sorry
-
-@[autograded 5]
-theorem problem2 (x : ℚ) : ∃ y : ℚ, y ^ 2 > x := by
-  sorry
-
-@[autograded 4]
-theorem problem3 {x : ℕ} (hx : Odd x) : Odd (x ^ 3) := by
-  sorry
-
-@[autograded 5]
-theorem problem4 (n : ℕ) : ∃ m ≥ n, Odd m := by
-  sorry
-
-@[autograded 2]
-theorem problem5 : (4 : ℤ) ∣ -12 := by
-  sorry
-
-@[autograded 2]
-theorem problem6 : ¬(3 : ℤ) ∣ -11 := by
-  sorry
-
-@[autograded 4]
-theorem problem7 {a b c : ℤ} (hab : a ^ 2 ∣ b) (hbc : b ^ 3 ∣ c) : a ^ 6 ∣ c := by
-  sorry
diff --git a/Math2001/Homework/hw4.lean b/Math2001/Homework/hw4.lean
deleted file mode 100644
index 67e59cc8..00000000
--- a/Math2001/Homework/hw4.lean
+++ /dev/null
@@ -1,40 +0,0 @@
-/- Copyright (c) Heather Macbeth, 2023.  All rights reserved. -/
-import Library.Basic
-import Library.Tactic.ModEq
-import AutograderLib
-
-math2001_init
-
-
-/-! # Homework 4
-
-Don't forget to compare with the text version,
-https://github.com/hrmacbeth/math2001/wiki/Homework-4,
-for clearer statements and any special instructions. -/
-
-
-@[autograded 4]
-theorem problem1 (h1 : a ≡ b [ZMOD n]) (h2 : b ≡ c [ZMOD n]) : a ≡ c [ZMOD n] := by
-  sorry
-
-@[autograded 4]
-theorem problem2 {t : ℤ} (h : t ≡ 2 [ZMOD 4]) :
-    3 * (t ^ 2 + t - 8) ≡ 3 * (2 ^ 2 + 2 - 8) [ZMOD 4] := by
-  sorry
-
-@[autograded 4]
-theorem problem3 {a : ℤ} (ha : a ≡ 3 [ZMOD 5]) :
-    a ^ 3 + 4 * a ^ 2 + 3 ≡ 1 [ZMOD 5] := by
-  sorry
-
-@[autograded 4]
-theorem problem4 : ∃ k : ℤ, k > 50 ∧ k ≡ 2 [ZMOD 5] ∧ 5 * k ≡ 6 [ZMOD 8] := by
-  sorry
-
-@[autograded 5]
-theorem problem5 {x : ℤ} : x ^ 5 ≡ x [ZMOD 5] := by
-  sorry
-
-@[autograded 4]
-theorem problem6 {n : ℤ} (h1 : 5 ∣ n) (h2 : 12 ∣ n) : 60 ∣ n := by
-  sorry
diff --git a/Math2001/Homework/hw5.lean b/Math2001/Homework/hw5.lean
deleted file mode 100644
index ad133c6b..00000000
--- a/Math2001/Homework/hw5.lean
+++ /dev/null
@@ -1,39 +0,0 @@
-/- Copyright (c) Heather Macbeth, 2023.  All rights reserved. -/
-import Mathlib.Data.Real.Basic
-import Library.Basic
-import Library.Tactic.ModEq
-import AutograderLib
-
--- BOTH:
-math2001_init
-
-/-! # Homework 5
-
-Don't forget to compare with the text version,
-https://github.com/hrmacbeth/math2001/wiki/Homework-5,
-for clearer statements and any special instructions. -/
-
-@[autograded 4]
-theorem problem1 : ∃ a : ℝ, ∀ b : ℝ, ∃ c : ℝ, a + c < b := by
-  sorry
-
-@[autograded 4]
-theorem problem2 : forall_sufficiently_large x : ℝ, x ^ 3 - 3 * x ≥ 12 * x ^ 2 := by
-  dsimp
-  sorry
-
-@[autograded 3]
-theorem problem3 (x : ℝ) : 3 * x + 1 = 10 ↔ x = 3 := by
-  sorry
-
-@[autograded 6]
-theorem problem4 (n : ℤ) : n ^ 2 + n + 3 ≡ 0 [ZMOD 5] ↔ n ≡ 1 [ZMOD 5] ∨ n ≡ 3 [ZMOD 5] := by
-  sorry
-
-@[autograded 4]
-theorem problem5 : ¬ (∃ t : ℝ, 2 * t ≤ 8 ∧ t ≥ 5) := by
-  sorry
-
-@[autograded 4]
-theorem problem6 : ¬ (∃ a : ℝ, ∀ b : ℝ, a ≤ b) := by
-  sorry
diff --git a/Math2001/Homework/hw6.lean b/Math2001/Homework/hw6.lean
deleted file mode 100644
index 7e4737be..00000000
--- a/Math2001/Homework/hw6.lean
+++ /dev/null
@@ -1,44 +0,0 @@
-/- Copyright (c) Heather Macbeth, 2023.  All rights reserved. -/
-import Mathlib.Data.Real.Basic
-import Library.Basic
-import Library.Tactic.ModEq
-import AutograderLib
-
-math2001_init
-set_option pp.funBinderTypes true
-
-/-! # Homework 6
-
-Don't forget to compare with the text version,
-https://github.com/hrmacbeth/math2001/wiki/Homework-6,
-for clearer statements and any special instructions. -/
-
-
-@[autograded 4]
-theorem problem1 (P Q : Prop) : (P ∨ Q) ↔ (Q ∨ P) := by
-  sorry
-
-@[autograded 5]
-theorem problem2 (P : α → Prop) (Q : Prop) : ((∃ x, P x) ∧ Q) ↔ ∃ x, (P x ∧ Q) := by
-  sorry
-
-@[autograded 5]
-theorem problem3 (P Q : Prop) : ¬ (P → Q) ↔ (P ∧ ¬ Q) := by
-  sorry
-
-@[autograded 3]
-theorem problem4 : ¬ (∀ x : ℝ, x ^ 2 ≥ x) := by
-  push_neg
-  sorry
-
-@[autograded 4]
-theorem problem5 : ¬ Int.Even 7 := by
-  dsimp [Int.Even]
-  push_neg
-  sorry
-
-@[autograded 4]
-theorem problem6 {p : ℕ} (k : ℕ) (hk1 : k ≠ 1) (hkp : k ≠ p) (hk : k ∣ p) : ¬ Prime p := by
-  dsimp [Prime]
-  push_neg
-  sorry
diff --git a/Math2001/Homework/hw7.lean b/Math2001/Homework/hw7.lean
deleted file mode 100644
index 430ecec1..00000000
--- a/Math2001/Homework/hw7.lean
+++ /dev/null
@@ -1,59 +0,0 @@
-/- Copyright (c) Heather Macbeth, 2023.  All rights reserved. -/
-import Mathlib.Tactic.GCongr
-import Library.Basic
-import Library.Tactic.ModEq
-import AutograderLib
-
-math2001_init
-
-
-/-! # Homework 7
-
-Don't forget to compare with the text version,
-https://github.com/hrmacbeth/math2001/wiki/Homework-7,
-for clearer statements and any special instructions. -/
-
-
-
-@[autograded 4]
-theorem problem1 (n : ℕ) : 5 ^ n ≡ 1 [ZMOD 8] ∨ 5 ^ n ≡ 5 [ZMOD 8] := by
-  sorry
-
-@[autograded 4]
-theorem problem2 : forall_sufficiently_large n : ℕ, (3:ℤ) ^ n ≥ 2 ^ n + 100 := by
-  dsimp
-  sorry
-
-def y : ℕ → ℕ
-  | 0 => 2
-  | n + 1 => (y n) ^ 2
-
-@[autograded 4]
-theorem problem3 (n : ℕ) : y n = 2 ^ (2 ^ n) := by
-  sorry
-
-def B : ℕ → ℚ
-  | 0 => 0
-  | n + 1 => B n + (n + 1 : ℚ) ^ 2
-
-@[autograded 4]
-theorem problem4 (n : ℕ) : B n = n * (n + 1) * (2 * n + 1) / 6 := by
-  sorry
-
-def b : ℕ → ℤ
-  | 0 => 0
-  | 1 => 1
-  | n + 2 => 5 * b (n + 1) - 6 * b n
-
-@[autograded 4]
-theorem problem5 (n : ℕ) : b n = 3 ^ n - 2 ^ n := by
-  sorry
-
-def r : ℕ → ℤ
-  | 0 => 2
-  | 1 => 0
-  | n + 2 => 2 * r (n + 1) + r n
-
-@[autograded 5]
-theorem problem6 : forall_sufficiently_large n : ℕ, r n ≥ 2 ^ n := by
-  sorry
diff --git a/Math2001/Homework/hw8.lean b/Math2001/Homework/hw8.lean
deleted file mode 100644
index 9e001be0..00000000
--- a/Math2001/Homework/hw8.lean
+++ /dev/null
@@ -1,21 +0,0 @@
-/- Copyright (c) Heather Macbeth, 2024.  All rights reserved. -/
-import Mathlib.Tactic.GCongr
-import Library.Basic
-import AutograderLib
-
-math2001_init
-
-/-! # Homework 8
-
-Don't forget to compare with the text version,
-https://github.com/hrmacbeth/math2001/wiki/Homework-8,
-for clearer statements and any special instructions. -/
-
-
-@[autograded 4]
-theorem problem3 (m : ℤ) (hn : 66 ∣ 41 * m) : 66 ∣ m := by
-  sorry
-
-@[autograded 6]
-theorem problem4 (a : ℤ) : 3333 ∣ a ↔ (101 ∣ a ∧ 33 ∣ a) := by
-  sorry
diff --git a/Math2001/Homework/hw9.lean b/Math2001/Homework/hw9.lean
deleted file mode 100644
index 80c9a551..00000000
--- a/Math2001/Homework/hw9.lean
+++ /dev/null
@@ -1,49 +0,0 @@
-/- Copyright (c) Heather Macbeth, 2023-4.  All rights reserved. -/
-import Mathlib.Data.Real.Basic
-import Library.Theory.InjectiveSurjective
-import Library.Basic
-import AutograderLib
-
-math2001_init
-set_option pp.funBinderTypes true
-
-open Function
-
-
-/-! # Homework 9
-
-Don't forget to compare with the text version,
-https://github.com/hrmacbeth/math2001/wiki/Homework-9,
-for clearer statements and any special instructions. -/
-
-@[autograded 3]
-theorem problem1 {f : X → Y} (hf : Injective f) {g : Y → Z} (hg : Injective g) :
-    Injective (g ∘ f) := by
-  sorry
-
-@[autograded 4]
-theorem problem2a : Bijective (fun (x : ℝ) ↦ 5 + 3 * x) := by
-  sorry
-
-@[autograded 4]
-theorem problem2b : ¬ Bijective (fun (x : ℝ) ↦ 5 + 3 * x) := by
-  sorry
-
-@[autograded 5]
-theorem problem3 :
-    ¬Injective (fun ((x, y, z) : ℝ × ℝ × ℝ) ↦ (x + y + z, x - 2 * y + z)) := by
-  sorry
-
-@[autograded 4]
-theorem problem4 : Bijective (fun ((r, s) : ℚ × ℚ) ↦ (s, r + 2 * s)) := by
-  rw [bijective_iff_exists_inverse]
-  use fun (a, b) ↦ (sorry, sorry)
-  sorry
-
-@[autograded 4]
-theorem problem5 : ¬ Surjective (fun ((x, y) : ℚ × ℚ) ↦ x ^ 2 + y ^ 2) := by
-  sorry
-
-@[autograded 5]
-theorem problem6 : Surjective (fun ((x, y) : ℚ × ℚ) ↦ x ^ 2 - y ^ 2) := by
-  sorry
diff --git a/lakefile.lean b/lakefile.lean
index c61e6baa..3cf801e4 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -29,4 +29,4 @@ but currently only Lean core options can be set in lakefile
 
 require mathlib from git "https://github.com/leanprover-community/mathlib4" @ s!"v{Lean.versionString}"
 require Duper from git "https://github.com/hrmacbeth/duper" @ "main"
-require autograder from git "https://github.com/robertylewis/lean4-autograder-main" @ "master"
+require autograder from git "https://github.com/robertylewis/lean4-autograder-main" @ "864b34ce06d8536aec0c38e57448c17d1f83572a"