diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index a37148a..1657ef5 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -26,6 +26,9 @@ jobs:
       - name: Build
         run: lake build
 
+      - name: Run Leanlings regressions
+        run: lake env lean --run tests/LeanlingsRegression.lean
+
       # The `nng` course's solutions form a Lean library, so they are already
       # compiled (and thus verified) by `lake build` above. Here we check the
       # standalone `intro` solutions, compiled file-by-file together with each
@@ -51,3 +54,8 @@ jobs:
             exit 1
           fi
           echo "All intro solutions verified against their checks"
+
+      - name: Verify intro IO output
+        run: |
+          diff -u <(printf 'Hello, Lean!\n') <(lean --run courses/intro/solutions/15_io/io1.lean)
+          diff -u <(printf '5\n4\n3\n2\n1\n') <(lean --run courses/intro/solutions/15_io/io2.lean)
diff --git a/Leanlings/Config.lean b/Leanlings/Config.lean
index a71f0ae..4b4be4c 100644
--- a/Leanlings/Config.lean
+++ b/Leanlings/Config.lean
@@ -126,9 +126,11 @@ private def introExercises : Array Exercise := #[
 
   -- 15_io
   { name := "io1", dir := "15_io",
-    hint := "`s!\"text {variable} text\"` is string interpolation.\n`IO.println` prints a line to the console." },
+    hint := "`s!\"text {variable} text\"` is string interpolation.\n`IO.println` prints a line to the console.",
+    expectedOutput := some "Hello, Lean!\n" },
   { name := "io2", dir := "15_io",
-    hint := "`List.range n` gives `[0, 1, ..., n-1]`.\nUse a `for` loop to iterate over it and print." },
+    hint := "`List.range n` gives `[0, 1, ..., n-1]`.\nUse a `for` loop to iterate over it and print.",
+    expectedOutput := some "5\n4\n3\n2\n1\n" },
 
   -- 16_implicit
   { name := "implicit1", dir := "16_implicit",
@@ -573,7 +575,7 @@ private def algebraExercises : Array Exercise := #[
     hint := "Re-associate, then commute the whole product." },
   { name := "sq_expand", dir := "CommRing",
     hint := "Expand with `mul_add_mul`, then commute the `b * a` term to `a * b`." },
-  -- Field
+  -- RealField
   { name := "mul_inv_cancel", dir := "RealField",
     hint := "This is exactly the field axiom for nonzero `a`." },
   { name := "inv_mul_cancel", dir := "RealField",
@@ -764,8 +766,8 @@ private def analysisWelcome : String :=
   "You will build the rational and real numbers from the ground up — no Mathlib —\n" ++
   "and develop their theory through Cauchy sequences toward the completeness of ℝ.\n\n" ++
   "The path: construct ℚ as a quotient of fractions (proving the equivalence\n" ++
-  "relation and that the operations are well defined), develop its ordered-field\n" ++
-  "theory (order, absolute value, the Archimedean property, density), build Cauchy\n" ++
+  "relation and that the operations are well defined), develop its arithmetic\n" ++
+  "and order theory (absolute value, the Archimedean property, density), build Cauchy\n" ++
   "sequences, and assemble ℝ as their quotient.\n\n" ++
   "Two ideas recur. (1) A statement about ℚ reduces, via `mk_eq` and the\n" ++
   "computation lemmas, to one about integers that `grind`/`omega` close. (2) A\n" ++
@@ -781,8 +783,9 @@ private def analysisFinal : String :=
   "Along the way you proved:\n" ++
   "  - that cross-multiplication is an equivalence relation, and that +, ×, −, <,\n" ++
   "    ≤ respect it, so they descend to the quotient ℚ;\n" ++
-  "  - the ordered-field theory of ℚ: the field axioms, trichotomy, the triangle\n" ++
-  "    inequality, the Archimedean property, and density;\n" ++
+  "  - the arithmetic and order theory of ℚ: algebraic laws (including inverse\n" ++
+  "    cancellation), trichotomy, the triangle inequality, the Archimedean\n" ++
+  "    property, and density;\n" ++
   "  - that constant, sum, negation sequences are Cauchy and that `CauchyEquiv` is\n" ++
   "    an equivalence relation;\n" ++
   "  - the ring theory of ℝ, built as the quotient of Cauchy sequences, with ℚ\n" ++
@@ -791,11 +794,11 @@ private def analysisFinal : String :=
   "    converges, in ℝ, to the real number it represents;\n" ++
   "  - the basics of abstract metric spaces (with ℝ as the example): that a\n" ++
   "    convergent sequence is Cauchy, proven from the axioms alone;\n" ++
-  "  - that ℝ is a field — every nonzero real has a multiplicative inverse;\n" ++
+  "  - that every nonzero real satisfies the inverse law `x * x⁻¹ = 1`;\n" ++
   "  - and the summit: ℝ is Cauchy-complete — every Cauchy sequence of reals\n" ++
   "    converges — proven by rational approximation.\n\n" ++
-  "You have built the real numbers from nothing and proved they are a complete\n" ++
-  "ordered field. That is the foundation the whole of real analysis rests on.\n"
+  "You have built the real numbers from nothing as a Cauchy-complete metric\n" ++
+  "space with commutative-ring operations and inverses for nonzero elements.\n"
 
 /-- Real analysis from scratch: construct ℚ and ℝ (via Cauchy sequences) in core
 Lean, then develop their theory. -/
@@ -806,6 +809,14 @@ def analysis : Course :=
 
 def courses : Array Course := #[intro, nng, algebra, analysis]
 
+/-- Qualified exercise ids must be unique within each course; otherwise progress
+tracking would be ambiguous again. -/
+private def hasUniqueExerciseIds (course : Course) : Bool :=
+  course.exercises.all fun exercise =>
+    (course.exercises.filter (·.id == exercise.id)).size == 1
+
+#guard courses.all hasUniqueExerciseIds
+
 /-- The course used when none is selected or a stored selection is invalid. -/
 def defaultCourse : Course := intro
 
diff --git a/Leanlings/Course.lean b/Leanlings/Course.lean
index a40c3be..a2b911b 100644
--- a/Leanlings/Course.lean
+++ b/Leanlings/Course.lean
@@ -29,9 +29,27 @@ def mkCourse (id title description : String) (exercises : Array Exercise)
 
 namespace Course
 
-/-- Find an exercise within this course by name. -/
-def getExercise (c : Course) (name : String) : Option Exercise :=
-  c.exercises.find? (·.name == name)
+/-- All exercises with a given bare name. -/
+def exercisesNamed (c : Course) (name : String) : Array Exercise :=
+  c.exercises.filter (·.name == name)
+
+/-- Whether a bare exercise name needs qualification in this course. -/
+def isAmbiguousName (c : Course) (name : String) : Bool :=
+  (c.exercisesNamed name).size > 1
+
+/-- Find an exercise by its qualified `dir/name` id, or by a bare name when that
+name is unique in the course. Ambiguous bare names deliberately fail instead of
+silently selecting the first exercise. -/
+def getExercise (c : Course) (target : String) : Option Exercise :=
+  match c.exercises.find? (·.id == target) with
+  | some exercise => some exercise
+  | none =>
+    let candidates := c.exercisesNamed target
+    if candidates.size == 1 then candidates[0]? else none
+
+/-- The shortest label that still identifies this exercise in its course. -/
+def displayName (c : Course) (exercise : Exercise) : String :=
+  if c.isAmbiguousName exercise.name then exercise.id else exercise.name
 
 end Course
 end Leanlings
diff --git a/Leanlings/Exercise.lean b/Leanlings/Exercise.lean
index ec1092e..3615fe8 100644
--- a/Leanlings/Exercise.lean
+++ b/Leanlings/Exercise.lean
@@ -14,10 +14,18 @@ structure Exercise where
   /-- The id of the course this exercise belongs to. Stamped by `mkCourse`. -/
   course : String := ""
   hint : String := ""
+  /-- Exact stdout expected when this exercise is executed with `lean --run`.
+  Most exercises are compile-time tasks and leave this unset. -/
+  expectedOutput : Option String := none
   deriving Repr, BEq, Inhabited
 
 namespace Exercise
 
+/-- The exercise's course-local, unambiguous identifier. Bare names remain
+accepted by the CLI when they identify exactly one exercise in a course. -/
+def id (e : Exercise) : String :=
+  s!"{e.dir}/{e.name}"
+
 def path (e : Exercise) : System.FilePath :=
   s!"courses/{e.course}/exercises/{e.dir}/{e.name}.lean"
 
diff --git a/Leanlings/Runner.lean b/Leanlings/Runner.lean
index da78fb3..925a840 100644
--- a/Leanlings/Runner.lean
+++ b/Leanlings/Runner.lean
@@ -20,6 +20,29 @@ private def runLean (path : System.FilePath) : IO ExerciseStatus := do
     return .compileError (output.stdout ++ output.stderr)
   return .success
 
+private def normalizeNewlines (s : String) : String :=
+  s.replace "\r\n" "\n"
+
+/-- Execute an IO exercise and compare its stdout with the contract in its
+metadata. This catches programs that merely type-check without doing the task. -/
+private def checkProgramOutput (exercise : Exercise) (expected : String) :
+    IO ExerciseStatus := do
+  let output ← IO.Process.output {
+    cmd := "lake"
+    args := #["env", "lean", "--run", exercise.path.toString]
+  }
+  if output.exitCode != 0 then
+    return .compileError
+      ("Your code compiles, but running it failed:\n" ++ output.stdout ++ output.stderr)
+  let actual := normalizeNewlines output.stdout
+  let expected := normalizeNewlines expected
+  if actual == expected then
+    return .success
+  return .compileError
+    ("Your code compiles, but it prints the wrong output.\n" ++
+     s!"Expected: {reprStr expected}\n" ++
+     s!"Actual:   {reprStr actual}")
+
 /-- Check a single exercise.
 
 Compiles via `lake env lean` so exercises that `import` a course library (e.g.
@@ -33,13 +56,15 @@ answers aren't shown to the learner. We check in two phases:
    real file with correct line numbers.
 2. If that is clean and a hidden test file exists, compile the exercise and the
    tests together. A failure here means the code type-checks but doesn't meet
-   the requirement; we say so without revealing the checks. -/
+   the requirement; we say so without revealing the checks.
+3. If the exercise declares expected output, execute it and compare stdout
+   exactly (apart from normalizing platform newline sequences). -/
 def checkExercise (exercise : Exercise) : IO ExerciseStatus := do
   match ← runLean exercise.path with
   | .success =>
     let testSrc ← (try some <$> IO.FS.readFile exercise.testPath catch _ => pure none)
     match testSrc with
-    | none => return .success
+    | none => pure ()
     | some tests =>
       let exSrc ← IO.FS.readFile exercise.path
       let tmp : System.FilePath := ".leanlings-check.lean"
@@ -47,11 +72,14 @@ def checkExercise (exercise : Exercise) : IO ExerciseStatus := do
       let result ← runLean tmp
       try IO.FS.removeFile tmp catch _ => pure ()
       match result with
-      | .success => return .success
+      | .success => pure ()
       | _ =>
         return .compileError
           "Your code compiles, but it doesn't satisfy the exercise's checks yet.\n\
            Re-read the task — the expected behaviour is described there."
+    match exercise.expectedOutput with
+    | some expected => checkProgramOutput exercise expected
+    | none => return .success
   | other => return other
 
 /-- Display the result of checking an exercise -/
diff --git a/Leanlings/State.lean b/Leanlings/State.lean
index 0adf6c8..033f118 100644
--- a/Leanlings/State.lean
+++ b/Leanlings/State.lean
@@ -5,8 +5,9 @@ namespace Leanlings
 
 /-- Persistent state tracking progress across courses.
 
-`completed` entries are namespaced as `"<courseId>/<exerciseName>"` so progress
-in one course never collides with another. `currentExercise` is a bare name
+`completed` entries are namespaced as `"<courseId>/<exerciseId>"`, where an
+exercise id is `"<dir>/<name>"`, so neither duplicate names within a course nor
+names shared by different courses collide. `currentExercise` is a qualified id
 within `currentCourse`. -/
 structure AppState where
   currentCourse : String
@@ -19,13 +20,48 @@ namespace AppState
 def stateFile : System.FilePath := ".leanlings-state"
 
 /-- The key under which an exercise's completion is recorded. -/
-def key (courseId name : String) : String := s!"{courseId}/{name}"
+def key (courseId exerciseId : String) : String := s!"{courseId}/{exerciseId}"
 
 def initial (course : Course) : AppState :=
   { currentCourse := course.id,
-    currentExercise := (course.exercises.getD 0 default).name,
+    currentExercise := (course.exercises.getD 0 default).id,
     completed := #[] }
 
+/-- Upgrade one completion key from the old `course/name` format to
+`course/dir/name`. For an old ambiguous name, selecting the first matching
+exercise is conservative: that is the only exercise the old runner could
+resolve and check. Unknown keys are retained unchanged. -/
+def migrateCompletedKey (courses : Array Course) (stored : String) : String :=
+  match courses.findSome? fun course =>
+    let coursePrefix := s!"{course.id}/"
+    if stored.startsWith coursePrefix then
+      let target := stored.drop coursePrefix.length
+      match course.exercises.find? (·.id == target) with
+      | some exercise => some (key course.id exercise.id)
+      | none =>
+        match course.exercises.find? (·.name == target) with
+        | some exercise => some (key course.id exercise.id)
+        | none => none
+    else
+      none
+  with
+  | some migrated => migrated
+  | none => stored
+
+/-- Migrate and deduplicate all stored completion keys. -/
+def normalizeCompleted (courses : Array Course) (stored : Array String) : Array String :=
+  stored.foldl (fun completed oldKey =>
+    let newKey := migrateCompletedKey courses oldKey
+    if completed.contains newKey then completed else completed.push newKey) #[]
+
+/-- Resolve either a current qualified id or a current name from an older state
+file. Legacy ambiguous names select the first exercise for the same reason as
+`migrateCompletedKey`. -/
+private def resolveStoredExercise (course : Course) (stored : String) : Option Exercise :=
+  match course.exercises.find? (·.id == stored) with
+  | some exercise => some exercise
+  | none => course.exercises.find? (·.name == stored)
+
 /-- Load state from disk, or return initial state if no (valid) state file exists.
 
 A stored course or exercise that no longer exists is repaired to a sensible
@@ -36,15 +72,17 @@ def load (courses : Array Course) (defaultCourse : Course) : IO AppState := do
     let lines := (content.splitOn "\n").filter (· != "")
     match lines with
     | course :: current :: rest =>
-      let completed := (rest.filter (· != "---")).toArray
+      let completed := normalizeCompleted courses (rest.filter (· != "---")).toArray
       let validCourse := if courses.any (·.id == course) then course else defaultCourse.id
       let activeCourse := (courses.find? (·.id == validCourse)).getD defaultCourse
       let validCurrent :=
-        if activeCourse.exercises.any (·.name == current) then current
-        else match activeCourse.exercises.findSome? (fun ex =>
-               if !completed.contains (key validCourse ex.name) then some ex.name else none) with
-             | some name => name
-             | none => (activeCourse.exercises.getD 0 default).name
+        match resolveStoredExercise activeCourse current with
+        | some exercise => exercise.id
+        | none =>
+          match activeCourse.exercises.findSome? (fun ex =>
+            if !completed.contains (key validCourse ex.id) then some ex.id else none) with
+          | some exerciseId => exerciseId
+          | none => (activeCourse.exercises.getD 0 default).id
       pure { currentCourse := validCourse, currentExercise := validCurrent, completed }
     | _ => pure (initial defaultCourse)
   catch _ =>
@@ -57,31 +95,31 @@ def save (state : AppState) : IO Unit := do
   IO.FS.writeFile stateFile content
 
 /-- Check if an exercise in the given course has been completed -/
-def isCompleted (state : AppState) (courseId name : String) : Bool :=
-  state.completed.contains (key courseId name)
+def isCompleted (state : AppState) (courseId exerciseId : String) : Bool :=
+  state.completed.contains (key courseId exerciseId)
 
 /-- Mark an exercise in the given course as completed -/
-def markCompleted (state : AppState) (courseId name : String) : AppState :=
-  let k := key courseId name
+def markCompleted (state : AppState) (courseId exerciseId : String) : AppState :=
+  let k := key courseId exerciseId
   if state.completed.contains k then state
   else { state with completed := state.completed.push k }
 
 /-- Mark an exercise as not completed (used by `reset`). -/
-def markIncomplete (state : AppState) (courseId name : String) : AppState :=
-  { state with completed := state.completed.filter (· != key courseId name) }
+def markIncomplete (state : AppState) (courseId exerciseId : String) : AppState :=
+  { state with completed := state.completed.filter (· != key courseId exerciseId) }
 
 /-- Switch the active course, moving to its first pending exercise. -/
 def switchCourse (state : AppState) (course : Course) : AppState :=
   let current := match course.exercises.findSome? (fun ex =>
-                   if !state.completed.contains (key course.id ex.name) then some ex.name else none) with
-                 | some name => name
-                 | none => (course.exercises.getD 0 default).name
+                   if !state.completed.contains (key course.id ex.id) then some ex.id else none) with
+                 | some exerciseId => exerciseId
+                 | none => (course.exercises.getD 0 default).id
   { state with currentCourse := course.id, currentExercise := current }
 
 /-- Find the next pending exercise in the given course -/
 def findNextPending (state : AppState) (course : Course) : Option String :=
   course.exercises.findSome? fun ex =>
-    if !state.completed.contains (key course.id ex.name) then some ex.name else none
+    if !state.completed.contains (key course.id ex.id) then some ex.id else none
 
 /-- Mark current exercise done and advance to next pending in the course -/
 def advance (state : AppState) (course : Course) : AppState :=
@@ -93,11 +131,11 @@ def advance (state : AppState) (course : Course) : AppState :=
 /-- Count completed exercises in the given course -/
 def countDone (state : AppState) (course : Course) : Nat :=
   course.exercises.foldl (fun n ex =>
-    if state.completed.contains (key course.id ex.name) then n + 1 else n) 0
+    if state.completed.contains (key course.id ex.id) then n + 1 else n) 0
 
 /-- Check if all exercises in the given course are done -/
 def allDone (state : AppState) (course : Course) : Bool :=
-  course.exercises.all (fun ex => state.completed.contains (key course.id ex.name))
+  course.exercises.all (fun ex => state.completed.contains (key course.id ex.id))
 
 end AppState
 end Leanlings
diff --git a/Main.lean b/Main.lean
index cac3e51..86263d3 100644
--- a/Main.lean
+++ b/Main.lean
@@ -14,13 +14,13 @@ def showHelp : IO Unit := do
   IO.println "Commands:"
   IO.println "  (none)       Show current exercise and status"
   IO.println "  run          Check the current exercise"
-  IO.println "  run <name>   Check a specific exercise"
+  IO.println "  run <name>   Check a specific exercise (use dir/name if ambiguous)"
   IO.println "  watch        Watch mode, auto-checks on save"
   IO.println "  verify       Check all exercises in the current course"
   IO.println "  hint         Show a hint for the current exercise"
   IO.println "  hint <name>  Show a hint for a specific exercise"
   IO.println "  solution     Show the solution for the current exercise"
-  IO.println "  solution <n> Show the solution for a specific exercise"
+  IO.println "  solution <name> Show the solution for a specific exercise"
   IO.println "  list         List exercises in the current course with status"
   IO.println "  next         Move to the next exercise"
   IO.println "  reset        Reset the current exercise (requires git)"
@@ -28,6 +28,19 @@ def showHelp : IO Unit := do
   IO.println "  courses      List available courses"
   IO.println "  course <id>  Switch to another course"
   IO.println "  help         Show this help"
+  IO.println "\nIf a name is repeated, qualify it as dir/name (for example, Rat/add_comm)."
+
+/-- Explain a failed exercise lookup, including every qualified choice when a
+bare name occurs more than once in the active course. -/
+def showExerciseLookupError (course : Course) (target : String) : IO Unit := do
+  let candidates := course.exercisesNamed target
+  if candidates.size > 1 then
+    IO.println s!"{UI.red "Error"}: exercise name '{target}' is ambiguous in course '{course.id}'."
+    IO.println "Use one of these qualified names:"
+    for exercise in candidates do
+      IO.println s!"  {exercise.id}"
+  else
+    IO.println s!"{UI.red "Error"}: exercise '{target}' not found in course '{course.id}'"
 
 def showStatus : IO Unit := do
   let (state, course) ← loadActive
@@ -44,7 +57,7 @@ def showStatus : IO Unit := do
   else
     match course.getExercise state.currentExercise with
     | some ex =>
-      IO.println s!"Current exercise: {UI.bold ex.name}"
+      IO.println s!"Current exercise: {UI.bold (course.displayName ex)}"
       IO.println s!"  → {ex.path}"
       IO.println ""
       IO.println "Open this file in your editor and follow the instructions!"
@@ -56,19 +69,19 @@ def runExercise (name : String) : IO UInt32 := do
   let (state, course) ← loadActive
   match course.getExercise name with
   | some ex =>
-    IO.println s!"Checking {UI.bold ex.name}...\n"
+    IO.println s!"Checking {UI.bold (course.displayName ex)}...\n"
     let status ← Runner.checkExercise ex
     Runner.displayResult ex status
     match status with
     | .success =>
-      let state := state.markCompleted course.id name
+      let state := state.markCompleted course.id ex.id
       state.save
       IO.println s!"\n{UI.progressBar (state.countDone course) course.exercises.size}"
       IO.println s!"\nRun `lake exe leanlings next` to continue."
       return 0
     | _ => return 1
   | none =>
-    IO.println s!"{UI.red "Error"}: exercise '{name}' not found in course '{course.id}'"
+    showExerciseLookupError course name
     return 1
 
 def runCurrent : IO UInt32 := do
@@ -80,35 +93,37 @@ def showHint (target : Option String) : IO Unit := do
   let name := target.getD state.currentExercise
   match course.getExercise name with
   | some ex =>
-    IO.println s!"\n{UI.cyan "Hint"} for {UI.bold ex.name}:\n"
+    IO.println s!"\n{UI.cyan "Hint"} for {UI.bold (course.displayName ex)}:\n"
     IO.println ex.hint
   | none =>
-    IO.println s!"{UI.red "Error"}: exercise '{name}' not found in course '{course.id}'"
+    showExerciseLookupError course name
 
 def listExercises : IO Unit := do
   let (state, course) ← loadActive
   IO.println s!"\n{UI.bold "Exercises"} — {course.title}:\n"
   for ex in course.exercises do
-    let marker := if state.isCompleted course.id ex.name then UI.green "✓"
-                  else if state.currentExercise == ex.name then UI.yellow "→"
+    let marker := if state.isCompleted course.id ex.id then UI.green "✓"
+                  else if state.currentExercise == ex.id then UI.yellow "→"
                   else "  "
-    IO.println s!" {marker} {ex.name}"
+    IO.println s!" {marker} {course.displayName ex}"
   IO.println ""
   IO.println (UI.progressBar (state.countDone course) course.exercises.size)
 
 def nextExercise : IO Unit := do
   let (state, course) ← loadActive
-  let idx := course.exercises.findIdx? (·.name == state.currentExercise)
+  let idx := course.exercises.findIdx? (·.id == state.currentExercise)
   match idx with
   | some i =>
     if i + 1 < course.exercises.size then
       if !state.isCompleted course.id state.currentExercise then
-        IO.println s!"{UI.yellow "!"} Warning: current exercise '{state.currentExercise}' is not yet completed."
+        let currentLabel := (course.getExercise state.currentExercise).map
+          (course.displayName ·) |>.getD state.currentExercise
+        IO.println s!"{UI.yellow "!"} Warning: current exercise '{currentLabel}' is not yet completed."
         IO.println "  Skipping to next exercise anyway."
       let next := course.exercises[i + 1]!
-      let state := { state with currentExercise := next.name }
+      let state := { state with currentExercise := next.id }
       state.save
-      IO.println s!"Current exercise: {UI.bold next.name}"
+      IO.println s!"Current exercise: {UI.bold (course.displayName next)}"
       IO.println s!"  → {next.path}"
     else
       IO.println "You're already on the last exercise!"
@@ -126,17 +141,17 @@ def resetExercise (name : String) : IO UInt32 := do
     if result.exitCode == 0 then
       -- The file is back to `sorry`, so it's no longer solved: clear its
       -- completion and make it the current exercise again.
-      let state := (state.markIncomplete course.id name)
-      let state := { state with currentExercise := name }
+      let state := state.markIncomplete course.id ex.id
+      let state := { state with currentExercise := ex.id }
       state.save
-      IO.println s!"{UI.green "✓"} Reset {ex.name} to original state"
+      IO.println s!"{UI.green "✓"} Reset {course.displayName ex} to original state"
       return 0
     else
       IO.println s!"{UI.red "Error"}: Could not reset. Make sure you're in a git repository."
       IO.println s!"  You can manually look at {ex.solutionPath}"
       return 1
   | none =>
-    IO.println s!"{UI.red "Error"}: exercise '{name}' not found in course '{course.id}'"
+    showExerciseLookupError course name
     return 1
 
 def verifyAll : IO UInt32 := do
@@ -150,20 +165,21 @@ def verifyAll : IO UInt32 := do
     let status ← Runner.checkExercise ex
     match status with
     | .success =>
-      IO.println s!"  {UI.green "✓"} {ex.name}"
+      IO.println s!"  {UI.green "✓"} {course.displayName ex}"
       doneCount := doneCount + 1
-      state := state.markCompleted course.id ex.name
+      state := state.markCompleted course.id ex.id
     | .compileError _ =>
-      IO.println s!"  {UI.red "✗"} {ex.name}"
+      IO.println s!"  {UI.red "✗"} {course.displayName ex}"
     | .hasSorry =>
-      IO.println s!"  {UI.yellow "!"} {ex.name}"
+      IO.println s!"  {UI.yellow "!"} {course.displayName ex}"
   state.save
   IO.println s!"\n{UI.progressBar doneCount course.exercises.size}"
   if doneCount == course.exercises.size then
     IO.println s!"\n{course.final}"
+    return 0
   else
     IO.println s!"\n{doneCount}/{course.exercises.size} exercises completed."
-  return 0
+    return 1
 
 partial def watchLoop (course : Course) (state : AppState) (lastContent : String) (firstRun : Bool) : IO UInt32 := do
   if state.allDone course then
@@ -182,7 +198,7 @@ partial def watchLoop (course : Course) (state : AppState) (lastContent : String
       IO.print UI.clearScreen
       IO.println s!"{UI.bold "Leanlings"} — Watch Mode ({course.title})\n"
       IO.println s!"{UI.progressBar (state.countDone course) course.exercises.size}\n"
-      IO.println s!"Checking {UI.bold ex.name}...\n"
+      IO.println s!"Checking {UI.bold (course.displayName ex)}...\n"
       let status ← Runner.checkExercise ex
       Runner.displayResult ex status
       match status with
@@ -192,7 +208,9 @@ partial def watchLoop (course : Course) (state : AppState) (lastContent : String
         if state.allDone course then
           IO.println s!"\n{course.final}"
           return 0
-        IO.println s!"\nMoving to next exercise: {UI.bold state.currentExercise}"
+        let nextLabel := (course.getExercise state.currentExercise).map
+          (course.displayName ·) |>.getD state.currentExercise
+        IO.println s!"\nMoving to next exercise: {UI.bold nextLabel}"
         IO.sleep 500
         watchLoop course state "" true
       | _ =>
@@ -218,11 +236,11 @@ def showSolution (target : Option String) : IO Unit := do
   let name := target.getD state.currentExercise
   match course.getExercise name with
   | some ex =>
-    IO.println s!"\n{UI.yellow "Solution"} for {UI.bold ex.name}:\n"
+    IO.println s!"\n{UI.yellow "Solution"} for {UI.bold (course.displayName ex)}:\n"
     let content ← IO.FS.readFile ex.solutionPath
     IO.println content
   | none =>
-    IO.println s!"{UI.red "Error"}: exercise '{name}' not found in course '{course.id}'"
+    showExerciseLookupError course name
 
 def listCourses : IO Unit := do
   let (state, _) ← loadActive
@@ -242,10 +260,12 @@ def selectCourse (id : String) : IO UInt32 := do
     let state := state.switchCourse course
     state.save
     IO.println s!"{UI.green "✓"} Switched to course {UI.bold course.title}"
-    IO.println s!"Current exercise: {UI.bold state.currentExercise}"
     match course.getExercise state.currentExercise with
-    | some ex => IO.println s!"  → {ex.path}"
-    | none => pure ()
+    | some ex =>
+      IO.println s!"Current exercise: {UI.bold (course.displayName ex)}"
+      IO.println s!"  → {ex.path}"
+    | none =>
+      IO.println s!"Current exercise: {UI.bold state.currentExercise}"
     return 0
   | none =>
     IO.println s!"{UI.red "Error"}: course '{id}' not found"
diff --git a/README.md b/README.md
index 2efcb4f..52bfc74 100644
--- a/README.md
+++ b/README.md
@@ -45,7 +45,7 @@ you edit) and a `solutions/` directory (reference answers).
 - `analysis` (62 exercises): real analysis from the ground up. You construct the
   rational numbers as a quotient of fractions — proving cross-multiplication is
   an equivalence relation and that the arithmetic and order respect it — then
-  develop ℚ's ordered-field theory (field axioms, order, absolute value, the
+  develop ℚ's arithmetic and order theory (algebraic laws, absolute value, the
   triangle inequality, the Archimedean property, density), build Cauchy
   sequences, and assemble the real numbers as their quotient, with ℚ embedded as
   the constant sequences. The construction lives in `AnalysisLib` plus a chain of
@@ -80,10 +80,11 @@ fractions are equal. You prove `r` is an equivalence relation, and that `+`, `×
 `−`, `<`, `≤` respect it — exactly what lets them descend to the quotient `MyRat`
 (assembled for you in the infrastructure modules `Rat.Quotient` and `Rat.Ops`).
 
-The theory of ℚ (worlds `Rat`, `RatOrder`): the field axioms, then the order,
-the absolute value and its triangle inequality, the Archimedean property, and the
-density of ℚ in itself. Each reduces, through `mk_eq` and the computation lemmas,
-to an integer fact that `grind`/`omega` close.
+The theory of ℚ (worlds `Rat`, `RatOrder`): arithmetic laws (including inverse
+cancellation), then the order, the absolute value and its triangle inequality,
+the Archimedean property, and the density of ℚ in itself. Each reduces, through
+`mk_eq` and the computation lemmas, to an integer fact that `grind`/`omega`
+close.
 
 Constructing ℝ (worlds `Cauchy`, `Real`): you prove the constant, sum, and
 negation of Cauchy sequences are Cauchy and that the "difference tends to zero"
@@ -101,10 +102,11 @@ The capstone (world `Capstone`) is the payoff: ℝ is complete over ℚ — ever
 Cauchy sequence of rationals converges, in ℝ, to the real number it represents.
 A `Metric` world introduces abstract metric spaces (with ℝ as the example) and
 proves, generically from the axioms, that a convergent sequence is Cauchy; and a
-`Field` world proves every nonzero real has a multiplicative inverse. The summit
+`RealField` world proves the inverse law for every nonzero real. The summit
 is the `Complete` world: ℝ is Cauchy-complete — every Cauchy sequence of reals
-converges — proven by rational approximation. The whole tower, ℚ to a complete
-ordered field, is built from nothing but core Lean.
+converges — proven by rational approximation. The whole tower — from ℚ through
+a Cauchy-complete metric model of ℝ with commutative-ring operations and a
+nonzero inverse law — is built from nothing but core Lean.
 
 ## Getting started
 
@@ -139,6 +141,10 @@ lake exe leanlings courses   # list courses
 lake exe leanlings course X  # switch to course X
 ```
 
+Bare exercise names work when they are unique. If a course repeats a name, use
+the `dir/name` shown by `list` or by the ambiguity error, such as
+`Rat/add_comm`.
+
 ## Other places to learn Lean 4
 
 A few resources worth knowing about, depending on what you are after:
diff --git a/courses/analysis/exercises/Rat/add_comm.lean b/courses/analysis/exercises/Rat/add_comm.lean
index 5f57ba7..50824d2 100644
--- a/courses/analysis/exercises/Rat/add_comm.lean
+++ b/courses/analysis/exercises/Rat/add_comm.lean
@@ -3,7 +3,7 @@ import Rat.Ops
 namespace Analysis
 open MyRat
 
-/- # Rat world — the field laws of ℚ
+/- # Rat world — the arithmetic laws of ℚ
 
 `Rat.Ops` now gives every operation on `MyRat`, plus the API you will use
 constantly:
diff --git a/courses/analysis/exercises/RealField/mul_inv_cancel.lean b/courses/analysis/exercises/RealField/mul_inv_cancel.lean
index 8940303..25af309 100644
--- a/courses/analysis/exercises/RealField/mul_inv_cancel.lean
+++ b/courses/analysis/exercises/RealField/mul_inv_cancel.lean
@@ -3,7 +3,7 @@ import Real.Inv
 namespace Analysis
 open MyReal
 
-/- # Field world — ℝ is a field
+/- # RealField world — inverses for nonzero reals
 
 `Real.Inv` constructs the multiplicative inverse on ℝ (the hardest piece, given
 in full): a nonzero real is *apart* from `0` (`CauSeq.apart` — some representative
@@ -12,7 +12,7 @@ provides:
   • `mk_eq_zero_iff : mk f hf = 0 ↔ CauSeq.Null ⟨f, hf⟩`;
   • `inv_mk_of_not_null hnn : (mk f hf)⁻¹ = mk (fun n => (f n)⁻¹) _`.
 
-Prove the field axiom: a nonzero real times its inverse is `1`. After
+Prove the nonzero inverse law: a nonzero real times its inverse is `1`. After
 `induction x using MyReal.ind`, get apartness data `⟨q, hq, N, hN⟩` from
 `CauSeq.apart` (using `hnn : ¬ CauSeq.Null ⟨f, hf⟩`, which follows from `hx` and
 `mk_eq_zero_iff`). Rewrite the inverse with `inv_mk_of_not_null`, then `mul_mk`,
diff --git a/courses/analysis/solutions/Cauchy/Defs.lean b/courses/analysis/solutions/Cauchy/Defs.lean
index 9952c47..89e07f0 100644
--- a/courses/analysis/solutions/Cauchy/Defs.lean
+++ b/courses/analysis/solutions/Cauchy/Defs.lean
@@ -1,10 +1,10 @@
 /-
 Infrastructure (given): the analysis toolkit on ℚ, and the definitions of Cauchy
-sequences. With the ordered-field theory of `MyRat` in hand (which you proved),
-we record the handful of inequality lemmas that the ε–N arguments need, a
-decidable order and a binary `max`, and then define what it means for a sequence
-of rationals to be Cauchy. The `Cauchy` world then asks you to prove the basic
-facts about these sequences.
+sequences. With the arithmetic and order theory of `MyRat` in hand (which you
+proved), we record the handful of inequality lemmas that the ε–N arguments need,
+a decidable order and a binary `max`, and then define what it means for a
+sequence of rationals to be Cauchy. The `Cauchy` world then asks you to prove the
+basic facts about these sequences.
 -/
 import RatOrder.exists_between
 
diff --git a/courses/analysis/solutions/Real/Inv.lean b/courses/analysis/solutions/Real/Inv.lean
index fb515da..e8e4fc7 100644
--- a/courses/analysis/solutions/Real/Inv.lean
+++ b/courses/analysis/solutions/Real/Inv.lean
@@ -1,8 +1,8 @@
 /-
-Infrastructure (given): the multiplicative inverse on ℝ — the step that makes it
-a field. The idea: a real `x ≠ 0` has a representative that is eventually bounded
-away from `0` (the apartness lemma), so its termwise reciprocal is Cauchy. The
-inverse is `0` on the null sequences and the termwise reciprocal otherwise.
+Infrastructure (given): the multiplicative inverse on ℝ. The idea: a real
+`x ≠ 0` has a representative that is eventually bounded away from `0` (the
+apartness lemma), so its termwise reciprocal is Cauchy. The inverse is `0` on
+the null sequences and the termwise reciprocal otherwise.
 
 This is the most intricate construction in the course; it is given in full.
 -/
diff --git a/courses/analysis/solutions/Real/Order.lean b/courses/analysis/solutions/Real/Order.lean
index e193327..89df821 100644
--- a/courses/analysis/solutions/Real/Order.lean
+++ b/courses/analysis/solutions/Real/Order.lean
@@ -4,7 +4,8 @@ Infrastructure (given): the order on ℝ.
 A real is *positive* when some representative is eventually bounded below by a
 fixed positive rational (`CauSeq.Pos`); this respects `CauchyEquiv`
 (`pos_equiv`), so it descends to `MyReal.IsPos`. Then `x < y := IsPos (y - x)`
-and `x ≤ y := IsPos (y - x) ∨ x = y`.
+and `x ≤ y := Nonneg (y - x)`, where `Nonneg` means eventually bounded below
+by `-ε` for every positive rational `ε`.
 
 We also record the few ℚ "transposition" lemmas (`sub_lt_iff`, `le_sub_iff`, …)
 the well-definedness argument needs, and prove the basic order facts.
diff --git a/courses/intro/exercises/12_typeclasses/typeclasses2.lean b/courses/intro/exercises/12_typeclasses/typeclasses2.lean
index 4919477..c192135 100644
--- a/courses/intro/exercises/12_typeclasses/typeclasses2.lean
+++ b/courses/intro/exercises/12_typeclasses/typeclasses2.lean
@@ -10,8 +10,10 @@
     instance : Describable Nat where
       describe n := s!"the number {n}"
 
-  TODO: 1. Implement the `BEq` instance for `Suit`.
-        2. Implement the `Describable` instance for `Suit`.
+  TODO: 1. Implement the `BEq` instance for `Suit`. Two values should be equal
+           exactly when they use the same constructor.
+        2. Implement the `Describable` instance for `Suit`, returning "Hearts",
+           "Diamonds", "Clubs", and "Spades" respectively.
 -/
 
 inductive Suit where
diff --git a/courses/intro/exercises/15_io/io1.lean b/courses/intro/exercises/15_io/io1.lean
index fa6e4b1..1183f42 100644
--- a/courses/intro/exercises/15_io/io1.lean
+++ b/courses/intro/exercises/15_io/io1.lean
@@ -15,7 +15,11 @@
 
   TODO: 1. Implement `greet` to print "Hello, {name}!"
            using `IO.println` and string interpolation `s!"..."`.
-        2. Have `main` call `greet` with a name.
+        2. Have `main` call `greet "Lean"` exactly once.
+
+  Running this file should print exactly:
+
+    Hello, Lean!
 -/
 
 -- Print "Hello, {name}!" using IO.println and s!"..."
diff --git a/courses/intro/exercises/16_implicit/implicit2.lean b/courses/intro/exercises/16_implicit/implicit2.lean
index 3fe970d..00c8426 100644
--- a/courses/intro/exercises/16_implicit/implicit2.lean
+++ b/courses/intro/exercises/16_implicit/implicit2.lean
@@ -20,5 +20,6 @@
 -- Check if a list contains an element (needs BEq)
 def myContains [BEq α] (x : α) (l : List α) : Bool := sorry
 
--- Remove duplicates from a list (needs BEq)
+-- Remove duplicates, keeping each value's last occurrence and preserving order
+-- (needs BEq). For example: myDedup [1, 2, 1, 3, 2] = [1, 3, 2].
 def myDedup [BEq α] (l : List α) : List α := sorry
diff --git a/courses/intro/solutions/15_io/io1.lean b/courses/intro/solutions/15_io/io1.lean
index 47ce40b..c6c6407 100644
--- a/courses/intro/solutions/15_io/io1.lean
+++ b/courses/intro/solutions/15_io/io1.lean
@@ -3,4 +3,3 @@ def greet (name : String) : IO Unit :=
 
 def main : IO Unit := do
   greet "Lean"
-  greet "World"
diff --git a/courses/intro/tests/05_structures/structs1.lean b/courses/intro/tests/05_structures/structs1.lean
new file mode 100644
index 0000000..3a24d42
--- /dev/null
+++ b/courses/intro/tests/05_structures/structs1.lean
@@ -0,0 +1,3 @@
+-- Hidden correctness checks for this exercise (not shown to the learner).
+#guard alice.name == "Alice"
+#guard alice.age == 30
diff --git a/courses/intro/tests/06_inductive/inductive3.lean b/courses/intro/tests/06_inductive/inductive3.lean
index 19fd299..c341ccf 100644
--- a/courses/intro/tests/06_inductive/inductive3.lean
+++ b/courses/intro/tests/06_inductive/inductive3.lean
@@ -1,4 +1,8 @@
 -- Hidden correctness checks for this exercise (not shown to the learner).
 #guard isNum (.num 5) == true
 #guard isNum (.add (.num 1) (.num 2)) == false
-
+#guard isNum (.mul (.num 1) (.num 2)) == false
+#guard
+  match sampleExpr with
+  | .mul (.add (.num 2) (.num 3)) (.num 4) => true
+  | _ => false
diff --git a/courses/intro/tests/12_typeclasses/typeclasses2.lean b/courses/intro/tests/12_typeclasses/typeclasses2.lean
index cd431d5..83308f3 100644
--- a/courses/intro/tests/12_typeclasses/typeclasses2.lean
+++ b/courses/intro/tests/12_typeclasses/typeclasses2.lean
@@ -1,9 +1,25 @@
 -- Hidden correctness checks for this exercise (not shown to the learner).
 #guard (Suit.hearts == Suit.hearts) == true
+#guard (Suit.diamonds == Suit.diamonds) == true
+#guard (Suit.clubs == Suit.clubs) == true
+#guard (Suit.spades == Suit.spades) == true
 #guard (Suit.hearts == Suit.diamonds) == false
+#guard (Suit.hearts == Suit.clubs) == false
+#guard (Suit.hearts == Suit.spades) == false
+#guard (Suit.diamonds == Suit.hearts) == false
+#guard (Suit.diamonds == Suit.clubs) == false
+#guard (Suit.diamonds == Suit.spades) == false
+#guard (Suit.clubs == Suit.hearts) == false
+#guard (Suit.clubs == Suit.diamonds) == false
 #guard (Suit.clubs == Suit.spades) == false
+#guard (Suit.spades == Suit.hearts) == false
+#guard (Suit.spades == Suit.diamonds) == false
+#guard (Suit.spades == Suit.clubs) == false
 open Describable in
-#guard (describe Suit.hearts).length > 0
+#guard describe Suit.hearts == "Hearts"
 open Describable in
-#guard (describe Suit.diamonds).length > 0
-
+#guard describe Suit.diamonds == "Diamonds"
+open Describable in
+#guard describe Suit.clubs == "Clubs"
+open Describable in
+#guard describe Suit.spades == "Spades"
diff --git a/courses/intro/tests/16_implicit/implicit2.lean b/courses/intro/tests/16_implicit/implicit2.lean
index 72063c2..bf18ab3 100644
--- a/courses/intro/tests/16_implicit/implicit2.lean
+++ b/courses/intro/tests/16_implicit/implicit2.lean
@@ -2,4 +2,6 @@
 #guard myContains 3 [1, 2, 3] == true
 #guard myContains 4 [1, 2, 3] == false
 #guard myContains 1 ([] : List Nat) == false
-
+#guard myDedup [1, 2, 1, 3, 2] == [1, 3, 2]
+#guard myDedup [1, 2, 3] == [1, 2, 3]
+#guard myDedup ([] : List Nat) == []
diff --git a/tests/LeanlingsRegression.lean b/tests/LeanlingsRegression.lean
new file mode 100644
index 0000000..f6e5a8c
--- /dev/null
+++ b/tests/LeanlingsRegression.lean
@@ -0,0 +1,67 @@
+import Leanlings
+
+open Leanlings
+
+/-! Regression checks for course identity, state migration, and runner output. -/
+
+#guard Config.analysis.exercises.size == 62
+#guard (Config.analysis.getExercise "add_comm").isNone
+#guard (Config.analysis.getExercise "mul_inv_cancel").isNone
+#guard (Config.analysis.getExercise "Rat/add_comm").map (·.dir) == some "Rat"
+#guard (Config.analysis.getExercise "Real/add_comm").map (·.dir) == some "Real"
+#guard (Config.analysis.getExercise "RealField/mul_inv_cancel").map (·.dir) ==
+  some "RealField"
+#guard (Config.analysis.getExercise "ofRat_add").map (·.id) == some "Real/ofRat_add"
+
+def migratedLegacy : Array String :=
+  AppState.normalizeCompleted Config.courses
+    #["analysis/add_comm", "analysis/add_comm", "intro/intro1", "unknown/key"]
+
+#guard migratedLegacy ==
+  #["analysis/Rat/add_comm", "intro/00_intro/intro1", "unknown/key"]
+
+def oneDuplicateCompletion : AppState :=
+  { currentCourse := "analysis"
+    currentExercise := "Rat/add_comm"
+    completed := #["analysis/Rat/add_comm"] }
+
+#guard oneDuplicateCompletion.countDone Config.analysis == 1
+
+def stateAfterCauchy : AppState :=
+  { currentCourse := "analysis"
+    currentExercise := "Cauchy/equiv_trans"
+    completed := Config.analysis.exercises
+      |>.filter (fun exercise =>
+        #["Setoid", "WellDef", "Rat", "RatOrder", "Cauchy"].contains exercise.dir)
+      |>.map (fun exercise => AppState.key Config.analysis.id exercise.id) }
+
+#guard stateAfterCauchy.findNextPending Config.analysis == some "Real/add_comm"
+
+def stateAfterMetric : AppState :=
+  { currentCourse := "analysis"
+    currentExercise := "Metric/converges_isCauchySeq"
+    completed := Config.analysis.exercises
+      |>.filter (fun exercise => exercise.dir != "RealField" && exercise.dir != "Complete")
+      |>.map (fun exercise => AppState.key Config.analysis.id exercise.id) }
+
+#guard stateAfterMetric.findNextPending Config.analysis ==
+  some "RealField/mul_inv_cancel"
+
+private def outputFixture (name expected : String) : Exercise :=
+  { name
+    dir := "Runner"
+    course := "../tests/fixtures"
+    expectedOutput := some expected }
+
+def main : IO UInt32 := do
+  let goodStatus ← Runner.checkExercise (outputFixture "good" "expected\n")
+  let silentStatus ← Runner.checkExercise (outputFixture "silent" "expected\n")
+  match goodStatus, silentStatus with
+  | .success, .compileError message =>
+    if message.contains "prints the wrong output" then
+      return 0
+    IO.eprintln s!"Unexpected output mismatch diagnostic: {message}"
+    return 1
+  | _, _ =>
+    IO.eprintln s!"Unexpected runner statuses: {repr goodStatus}, {repr silentStatus}"
+    return 1
diff --git a/tests/fixtures/exercises/Runner/good.lean b/tests/fixtures/exercises/Runner/good.lean
new file mode 100644
index 0000000..972b390
--- /dev/null
+++ b/tests/fixtures/exercises/Runner/good.lean
@@ -0,0 +1,2 @@
+def main : IO Unit :=
+  IO.println "expected"
diff --git a/tests/fixtures/exercises/Runner/silent.lean b/tests/fixtures/exercises/Runner/silent.lean
new file mode 100644
index 0000000..b9be659
--- /dev/null
+++ b/tests/fixtures/exercises/Runner/silent.lean
@@ -0,0 +1,2 @@
+def main : IO Unit :=
+  pure ()