diff --git a/generators/Generator/Generator.lean b/generators/Generator/Generator.lean
index e761d32..1b473b6 100644
--- a/generators/Generator/Generator.lean
+++ b/generators/Generator/Generator.lean
@@ -100,6 +100,7 @@ import Generator.AnagramGenerator
 import Generator.BobGenerator
 import Generator.MatchingBracketsGenerator
 import Generator.ReverseStringGenerator
+import Generator.GameNightGenerator
 
 import Std
 import Lean.Data.Json
@@ -112,6 +113,7 @@ abbrev endBodyGenerator := String -> String
 
 def dispatch : Std.HashMap String (introGenerator × testCaseGenerator × endBodyGenerator) :=
   Std.HashMap.ofList [
+    ("GameNight", (GameNightGenerator.genIntro, GameNightGenerator.genTestCase, GameNightGenerator.genEnd)),
     ("MountainHike", (MountainHikeGenerator.genIntro, MountainHikeGenerator.genTestCase, MountainHikeGenerator.genEnd)),
     ("FruitStand", (FruitStandGenerator.genIntro, FruitStandGenerator.genTestCase, FruitStandGenerator.genEnd)),
     ("DotDsl", (DotDslGenerator.genIntro, DotDslGenerator.genTestCase, DotDslGenerator.genEnd)),
diff --git a/generators/Generator/Generator/GameNightGenerator.lean b/generators/Generator/Generator/GameNightGenerator.lean
new file mode 100644
index 0000000..a67d54e
--- /dev/null
+++ b/generators/Generator/Generator/GameNightGenerator.lean
@@ -0,0 +1,40 @@
+import Lean.Data.Json
+import Std
+import Helper
+
+open Lean
+open Std
+open Helper
+
+namespace GameNightGenerator
+
+def genIntro (exercise : String) : String := s!"import LeanTest
+import {exercise}
+
+open LeanTest
+
+def {exercise.decapitalize}Tests : TestSuite :=
+  (TestSuite.empty \"{exercise}\")"
+
+def genTestCase (exercise : String) (case : TreeMap.Raw String Json) : String :=
+  let input := case.get! "input"
+  let expected := case.get! "expected"
+  let description := case.get! "description"
+              |> (·.compress)
+  let funName := getFunName (case.get! "property")
+  let call := s!"({exercise}.{funName} {insertAllInputs input})"
+  let taskArg := match case.get? "task" with
+    | some task => s!" (taskId := some {task})"
+    | none => ""
+  s!"
+  |>.addTest {description} (do
+      return assertEqual {expected} {call}){taskArg}"
+
+def genEnd (exercise : String) : String :=
+  s!"
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [{exercise.decapitalize}Tests]
+"
+
+end GameNightGenerator
diff --git a/reference/concepts/booleans/.meta/config.json b/reference/concepts/booleans/.meta/config.json
new file mode 100644
index 0000000..75d5301
--- /dev/null
+++ b/reference/concepts/booleans/.meta/config.json
@@ -0,0 +1,6 @@
+{
+  "blurb": "Learn Lean's Bool type.",
+  "authors": [
+    "oxe-i"
+  ]
+}
diff --git a/reference/concepts/booleans/about.md b/reference/concepts/booleans/about.md
new file mode 100644
index 0000000..ecd04ce
--- /dev/null
+++ b/reference/concepts/booleans/about.md
@@ -0,0 +1,64 @@
+# About
+
+`Bool` is the type of truth values.
+It has two values, `true` and `false`.
+
+```lean
+#eval true  -- true
+```
+
+## Combining Bool values
+
+`&&` is "and". 
+It is `true` only when both sides are `true`.
+
+```lean
+#eval true && false -- false
+#eval true && true  -- true
+```
+
+`||` is "or". 
+It is `true` when at least one side is `true`.
+
+```lean
+#eval true || false -- true
+#eval false || false -- false
+```
+
+`!` is "not". 
+It flips a `Bool`, so that `true` becomes `false` and `false` becomes `true`.
+
+```lean
+#eval !true  -- false
+#eval !false -- true
+```
+
+`^^` is "xor" (exclusive or). 
+It is `true` when exactly one side is `true`.
+If both sides are `false` or both are `true`, it is `false`.
+
+```lean
+#eval true ^^ false -- true
+#eval true ^^ true  -- false
+```
+
+## Short-circuit evaluation
+
+`&&` does not look at its right side when the left side is `false`.
+`||` does not look at its right side when the left side is `true`.
+This is called short-circuit evaluation.
+
+For example, `false && (some slow check)` skips the slow check entirely.
+The result is already known to be `false` from the left side alone.
+
+`^^` cannot short-circuit because its result always depends on both sides.
+
+## Comparing Bool values
+
+`Bool` supports `==` and `!=`, like `Nat` and `Int` do.
+
+```lean
+#eval true == true   -- true
+#eval true == false  -- false
+#eval true != false  -- true
+```
diff --git a/reference/concepts/booleans/introduction.md b/reference/concepts/booleans/introduction.md
new file mode 100644
index 0000000..3a48521
--- /dev/null
+++ b/reference/concepts/booleans/introduction.md
@@ -0,0 +1,64 @@
+# Introduction
+
+`Bool` is the type of truth values.
+It has two values, `true` and `false`.
+
+```lean
+#eval true  -- true
+```
+
+## Combining Bool values
+
+`&&` is "and". 
+It is `true` only when both sides are `true`.
+
+```lean
+#eval true && false -- false
+#eval true && true  -- true
+```
+
+`||` is "or". 
+It is `true` when at least one side is `true`.
+
+```lean
+#eval true || false -- true
+#eval false || false -- false
+```
+
+`!` is "not". 
+It flips a `Bool`, so that `true` becomes `false` and `false` becomes `true`.
+
+```lean
+#eval !true  -- false
+#eval !false -- true
+```
+
+`^^` is "xor" (exclusive or). 
+It is `true` when exactly one side is `true`.
+If both sides are `false` or both are `true`, it is `false`.
+
+```lean
+#eval true ^^ false -- true
+#eval true ^^ true  -- false
+```
+
+## Short-circuit evaluation
+
+`&&` does not look at its right side when the left side is `false`.
+`||` does not look at its right side when the left side is `true`.
+This is called short-circuit evaluation.
+
+For example, `false && (some slow check)` skips the slow check entirely.
+The result is already known to be `false` from the left side alone.
+
+`^^` cannot short-circuit because its result always depends on both sides.
+
+## Comparing Bool values
+
+`Bool` supports `==` and `!=`, like `Nat` and `Int` do.
+
+```lean
+#eval true == true   -- true
+#eval true == false  -- false
+#eval true != false  -- true
+```
diff --git a/reference/concepts/booleans/links.json b/reference/concepts/booleans/links.json
new file mode 100644
index 0000000..efb08b7
--- /dev/null
+++ b/reference/concepts/booleans/links.json
@@ -0,0 +1,6 @@
+[
+  {
+    "url": "https://lean-lang.org/doc/reference/latest/Basic-Types/",
+    "description": "The Lean Language Reference: Basic Types, including Booleans"
+  }
+]
diff --git a/reference/config.json.additions b/reference/config.json.additions
index be5453b..2fa85aa 100644
--- a/reference/config.json.additions
+++ b/reference/config.json.additions
@@ -49,3 +49,27 @@
   ],
   "status": "beta"
 }
+
+// ---- booleans / game-night ----
+
+// Append to the top-level "concepts" array:
+{
+  "uuid": "5193a16c-2f38-48a6-8d23-c81fd5cd8a6e",
+  "slug": "booleans",
+  "name": "Booleans"
+}
+
+// Append to "exercises.concept":
+{
+  "slug": "game-night",
+  "name": "Game Night",
+  "uuid": "13718a3a-ad48-492a-951f-75e325c0537b",
+  "concepts": [
+    "booleans"
+  ],
+  "prerequisites": [
+    "basics",
+    "numbers"
+  ],
+  "status": "beta"
+}
diff --git a/reference/exercises/concept/fruit-stand/FruitStand.lean b/reference/exercises/concept/fruit-stand/FruitStand.lean
index 18fa491..35dfd29 100644
--- a/reference/exercises/concept/fruit-stand/FruitStand.lean
+++ b/reference/exercises/concept/fruit-stand/FruitStand.lean
@@ -1,6 +1,7 @@
 namespace FruitStand
 
-def applePrice : Nat := sorry --remove this line and define the constant
+def applePrice : Nat :=
+  sorry --remove this line and define the constant
 
 def revenue (applesSold : Nat) : Nat :=
   sorry --remove this line and implement the function
diff --git a/reference/exercises/concept/game-night/.docs/hints.md b/reference/exercises/concept/game-night/.docs/hints.md
new file mode 100644
index 0000000..f5c1392
--- /dev/null
+++ b/reference/exercises/concept/game-night/.docs/hints.md
@@ -0,0 +1,29 @@
+# Hints
+
+## General
+
+- [Basic Types][basic-types] in the Lean reference covers `Bool`, including `&&`, `||`, and `!`.
+- All five functions return a `Bool`, and need explicit parameter and return types, as usual.
+
+## 1. Check who can join
+
+- You can use [boolean operators][bool-operators] to combine the two parameters.
+
+## 2. Check who brings snacks
+
+- You can use [boolean operators][bool-operators] to combine the two parameters.
+
+## 3. Check who is skipping game night
+
+- You can use a [boolean operator][bool-operators] to invert the parameter.
+
+## 4. Check if two friends voted for the same game
+
+- Boolean values can be compared for equality.
+
+## 5. Check if there's exactly one scorekeeper
+
+- You can use [boolean operators][bool-operators] to combine the two parameters.
+
+[basic-types]: https://lean-lang.org/doc/reference/latest/Basic-Types/
+[bool-operators]: https://lean-lang.org/doc/reference/latest/Basic-Types/Booleans/#The-Lean-Language-Reference--Basic-Types--Booleans--Syntax
diff --git a/reference/exercises/concept/game-night/.docs/instructions.md b/reference/exercises/concept/game-night/.docs/instructions.md
new file mode 100644
index 0000000..5b67628
--- /dev/null
+++ b/reference/exercises/concept/game-night/.docs/instructions.md
@@ -0,0 +1,54 @@
+# Instructions
+
+You are helping organize a game night with friends.
+
+## 1. Check who can join
+
+Define `canJoin`, a function with two `Bool` parameters, `hasConfirmed` and `isInvited`.
+The function returns `true` only when both are `true`.
+
+```lean
+#eval canJoin true true   -- true
+#eval canJoin true false  -- false
+```
+
+## 2. Check who brings snacks
+
+Define `bringsSnacks`, a function with two `Bool` parameters, `isHost` and `volunteered`.
+The function returns `true` when at least one of them is `true`.
+
+```lean
+#eval bringsSnacks true false  -- true
+#eval bringsSnacks false false -- false
+```
+
+## 3. Check who is skipping game night
+
+Define `isSkipping`, a function with one `Bool` parameter, `isComing`.
+It returns the opposite of `isComing`.
+
+```lean
+#eval isSkipping true  -- false
+#eval isSkipping false -- true
+```
+
+## 4. Check if two friends voted for the same game
+
+Define `votedSame`, a function with two `Bool` parameters, `firstVote` and `secondVote`.
+Each vote is `true` for "board game" and `false` for "video game".
+It returns `true` when both friends voted for the same kind of game.
+
+```lean
+#eval votedSame true true   -- true
+#eval votedSame true false  -- false
+```
+
+## 5. Check if there's exactly one scorekeeper
+
+Define `hasScorekeeper`, a function with two `Bool` parameters, `aVolunteers` and `bVolunteers`.
+It returns `true` only when exactly one of them is `true`.
+
+```lean
+#eval hasScorekeeper true false -- true
+#eval hasScorekeeper true true  -- false
+```
diff --git a/reference/exercises/concept/game-night/.docs/introduction.md b/reference/exercises/concept/game-night/.docs/introduction.md
new file mode 100644
index 0000000..3a48521
--- /dev/null
+++ b/reference/exercises/concept/game-night/.docs/introduction.md
@@ -0,0 +1,64 @@
+# Introduction
+
+`Bool` is the type of truth values.
+It has two values, `true` and `false`.
+
+```lean
+#eval true  -- true
+```
+
+## Combining Bool values
+
+`&&` is "and". 
+It is `true` only when both sides are `true`.
+
+```lean
+#eval true && false -- false
+#eval true && true  -- true
+```
+
+`||` is "or". 
+It is `true` when at least one side is `true`.
+
+```lean
+#eval true || false -- true
+#eval false || false -- false
+```
+
+`!` is "not". 
+It flips a `Bool`, so that `true` becomes `false` and `false` becomes `true`.
+
+```lean
+#eval !true  -- false
+#eval !false -- true
+```
+
+`^^` is "xor" (exclusive or). 
+It is `true` when exactly one side is `true`.
+If both sides are `false` or both are `true`, it is `false`.
+
+```lean
+#eval true ^^ false -- true
+#eval true ^^ true  -- false
+```
+
+## Short-circuit evaluation
+
+`&&` does not look at its right side when the left side is `false`.
+`||` does not look at its right side when the left side is `true`.
+This is called short-circuit evaluation.
+
+For example, `false && (some slow check)` skips the slow check entirely.
+The result is already known to be `false` from the left side alone.
+
+`^^` cannot short-circuit because its result always depends on both sides.
+
+## Comparing Bool values
+
+`Bool` supports `==` and `!=`, like `Nat` and `Int` do.
+
+```lean
+#eval true == true   -- true
+#eval true == false  -- false
+#eval true != false  -- true
+```
diff --git a/reference/exercises/concept/game-night/.docs/introduction.md.tpl b/reference/exercises/concept/game-night/.docs/introduction.md.tpl
new file mode 100644
index 0000000..86967ed
--- /dev/null
+++ b/reference/exercises/concept/game-night/.docs/introduction.md.tpl
@@ -0,0 +1 @@
+%{concept: booleans}
diff --git a/reference/exercises/concept/game-night/.meta/Exemplar.lean b/reference/exercises/concept/game-night/.meta/Exemplar.lean
new file mode 100644
index 0000000..323dc30
--- /dev/null
+++ b/reference/exercises/concept/game-night/.meta/Exemplar.lean
@@ -0,0 +1,18 @@
+namespace GameNight
+
+def canJoin (hasConfirmed isInvited : Bool) : Bool :=
+  hasConfirmed && isInvited
+
+def bringsSnacks (isHost volunteered : Bool) : Bool :=
+  isHost || volunteered
+
+def isSkipping (isComing : Bool) : Bool :=
+  !isComing
+
+def votedSame (firstVote secondVote : Bool) : Bool :=
+  firstVote == secondVote
+
+def hasScorekeeper (aVolunteers bVolunteers : Bool) : Bool :=
+  aVolunteers ^^ bVolunteers
+
+end GameNight
diff --git a/reference/exercises/concept/game-night/.meta/config.json b/reference/exercises/concept/game-night/.meta/config.json
new file mode 100644
index 0000000..c2014f8
--- /dev/null
+++ b/reference/exercises/concept/game-night/.meta/config.json
@@ -0,0 +1,17 @@
+{
+  "authors": [
+    "oxe-i"
+  ],
+  "files": {
+    "solution": [
+      "GameNight.lean"
+    ],
+    "test": [
+      "GameNightTest.lean"
+    ],
+    "exemplar": [
+      ".meta/Exemplar.lean"
+    ]
+  },
+  "blurb": "Learn Lean's Bool type by organizing a game night."
+}
diff --git a/reference/exercises/concept/game-night/.meta/design.md b/reference/exercises/concept/game-night/.meta/design.md
new file mode 100644
index 0000000..c4b1a39
--- /dev/null
+++ b/reference/exercises/concept/game-night/.meta/design.md
@@ -0,0 +1,41 @@
+# Design
+
+## Goal
+
+The goal of this exercise is to teach the `Bool` type and its operators in Lean.
+
+## Learning objectives
+
+- Know that `Bool` has two values, `true` and `false`.
+- Know how to combine `Bool` values with `&&` and `||`.
+- Know how to negate a `Bool` value with `!`.
+- Know how to combine `Bool` values with `^^`.
+- Know how to compare `Bool` values with `==`.
+
+## Out of scope
+
+- Short-circuit evaluation is explained in the concept text, but not tested here.
+  Testing it would require observable side effects, which need `IO`, a much later concept.
+- `if`/`then`/`else` and other control flow (a later concept).
+- Any boolean operator not listed above.
+
+## Concepts
+
+`booleans`:
+
+- `Bool`, `true`, `false`
+- `&&`, `||`, `!`, `^^`
+- `==` on `Bool`
+
+## Prerequisites
+
+- `basics`
+- `numbers`
+
+## Representer
+
+This track has no representer.
+
+## Analyzer
+
+This track has no analyzer.
diff --git a/reference/exercises/concept/game-night/.meta/extra.json b/reference/exercises/concept/game-night/.meta/extra.json
new file mode 100644
index 0000000..25518c0
--- /dev/null
+++ b/reference/exercises/concept/game-night/.meta/extra.json
@@ -0,0 +1,100 @@
+[
+  {
+    "property": "canJoin",
+    "description": "Confirmed and invited can join",
+    "input": { "hasConfirmed": true, "isInvited": true },
+    "expected": true,
+    "task": 1
+  },
+  {
+    "property": "canJoin",
+    "description": "Confirmed but not invited cannot join",
+    "input": { "hasConfirmed": true, "isInvited": false },
+    "expected": false,
+    "task": 1
+  },
+  {
+    "property": "canJoin",
+    "description": "invited but has not confirmed cannot join",
+    "input": { "hasConfirmed": false, "isInvited": true },
+    "expected": false,
+    "task": 1
+  },
+  {
+    "property": "bringsSnacks",
+    "description": "host brings snacks",
+    "input": { "isHost": true, "volunteered": false },
+    "expected": true,
+    "task": 2
+  },
+  {
+    "property": "bringsSnacks",
+    "description": "volunteer brings snacks",
+    "input": { "isHost": false, "volunteered": true },
+    "expected": true,
+    "task": 2
+  },
+  {
+    "property": "bringsSnacks",
+    "description": "neither host nor volunteer brings no snacks",
+    "input": { "isHost": false, "volunteered": false },
+    "expected": false,
+    "task": 2
+  },
+  {
+    "property": "isSkipping",
+    "description": "coming is not skipping",
+    "input": { "isComing": true },
+    "expected": false,
+    "task": 3
+  },
+  {
+    "property": "isSkipping",
+    "description": "not coming is skipping",
+    "input": { "isComing": false },
+    "expected": true,
+    "task": 3
+  },
+  {
+    "property": "votedSame",
+    "description": "both voted for the board game",
+    "input": { "firstVote": true, "secondVote": true },
+    "expected": true,
+    "task": 4
+  },
+  {
+    "property": "votedSame",
+    "description": "voted for different games",
+    "input": { "firstVote": true, "secondVote": false },
+    "expected": false,
+    "task": 4
+  },
+  {
+    "property": "votedSame",
+    "description": "both voted for the video game",
+    "input": { "firstVote": false, "secondVote": false },
+    "expected": true,
+    "task": 4
+  },
+  {
+    "property": "hasScorekeeper",
+    "description": "exactly one volunteer is the scorekeeper",
+    "input": { "aVolunteers": true, "bVolunteers": false },
+    "expected": true,
+    "task": 5
+  },
+  {
+    "property": "hasScorekeeper",
+    "description": "both volunteering means no single scorekeeper",
+    "input": { "aVolunteers": true, "bVolunteers": true },
+    "expected": false,
+    "task": 5
+  },
+  {
+    "property": "hasScorekeeper",
+    "description": "neither volunteering means no scorekeeper",
+    "input": { "aVolunteers": false, "bVolunteers": false },
+    "expected": false,
+    "task": 5
+  }
+]
diff --git a/reference/exercises/concept/game-night/GameNight.lean b/reference/exercises/concept/game-night/GameNight.lean
new file mode 100644
index 0000000..4e16fa7
--- /dev/null
+++ b/reference/exercises/concept/game-night/GameNight.lean
@@ -0,0 +1,18 @@
+namespace GameNight
+
+def canJoin (hasConfirmed isInvited : Bool) : Bool :=
+  sorry --remove this line and implement the function
+
+def bringsSnacks (isHost volunteered : Bool) : Bool :=
+  sorry --remove this line and implement the function
+
+def isSkipping (isComing : Bool) : Bool :=
+  sorry --remove this line and implement the function
+
+def votedSame (firstVote secondVote : Bool) : Bool :=
+  sorry --remove this line and implement the function
+
+def hasScorekeeper (aVolunteers bVolunteers : Bool) : Bool :=
+  sorry --remove this line and implement the function
+
+end GameNight
diff --git a/reference/exercises/concept/game-night/GameNightTest.lean b/reference/exercises/concept/game-night/GameNightTest.lean
new file mode 100644
index 0000000..2c98960
--- /dev/null
+++ b/reference/exercises/concept/game-night/GameNightTest.lean
@@ -0,0 +1,38 @@
+import LeanTest
+import GameNight
+
+open LeanTest
+
+def gameNightTests : TestSuite :=
+  (TestSuite.empty "GameNight")
+  |>.addTest "Confirmed and invited can join" (do
+      return assertEqual true (GameNight.canJoin true true)) (taskId := some 1)
+  |>.addTest "Confirmed but not invited cannot join" (do
+      return assertEqual false (GameNight.canJoin true false)) (taskId := some 1)
+  |>.addTest "invited but has not confirmed cannot join" (do
+      return assertEqual false (GameNight.canJoin false true)) (taskId := some 1)
+  |>.addTest "host brings snacks" (do
+      return assertEqual true (GameNight.bringsSnacks true false)) (taskId := some 2)
+  |>.addTest "volunteer brings snacks" (do
+      return assertEqual true (GameNight.bringsSnacks false true)) (taskId := some 2)
+  |>.addTest "neither host nor volunteer brings no snacks" (do
+      return assertEqual false (GameNight.bringsSnacks false false)) (taskId := some 2)
+  |>.addTest "coming is not skipping" (do
+      return assertEqual false (GameNight.isSkipping true)) (taskId := some 3)
+  |>.addTest "not coming is skipping" (do
+      return assertEqual true (GameNight.isSkipping false)) (taskId := some 3)
+  |>.addTest "both voted for the board game" (do
+      return assertEqual true (GameNight.votedSame true true)) (taskId := some 4)
+  |>.addTest "voted for different games" (do
+      return assertEqual false (GameNight.votedSame true false)) (taskId := some 4)
+  |>.addTest "both voted for the video game" (do
+      return assertEqual true (GameNight.votedSame false false)) (taskId := some 4)
+  |>.addTest "exactly one volunteer is the scorekeeper" (do
+      return assertEqual true (GameNight.hasScorekeeper true false)) (taskId := some 5)
+  |>.addTest "both volunteering means no single scorekeeper" (do
+      return assertEqual false (GameNight.hasScorekeeper true true)) (taskId := some 5)
+  |>.addTest "neither volunteering means no scorekeeper" (do
+      return assertEqual false (GameNight.hasScorekeeper false false)) (taskId := some 5)
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [gameNightTests]
diff --git a/reference/exercises/concept/game-night/lakefile.toml b/reference/exercises/concept/game-night/lakefile.toml
new file mode 100644
index 0000000..1c1f622
--- /dev/null
+++ b/reference/exercises/concept/game-night/lakefile.toml
@@ -0,0 +1,19 @@
+name = "game-night"
+version = "0.1.0"
+defaultTargets = ["GameNightTest"]
+testDriver = "GameNightTest"
+moreLeanArgs = [ "-DwarningAsError=true" ]
+
+[[lean_lib]]
+name = "LeanTest"
+srcDir = "vendor/LeanTest"
+
+[[lean_lib]]
+name = "GameNight"
+
+[[lean_lib]]
+name = "Extra"
+
+[[lean_exe]]
+name = "GameNightTest"
+root = "GameNightTest"
diff --git a/reference/exercises/concept/game-night/lean-toolchain b/reference/exercises/concept/game-night/lean-toolchain
new file mode 100644
index 0000000..14791d7
--- /dev/null
+++ b/reference/exercises/concept/game-night/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.29.0
diff --git a/reference/exercises/concept/game-night/vendor/LeanTest/LeanTest.lean b/reference/exercises/concept/game-night/vendor/LeanTest/LeanTest.lean
new file mode 100644
index 0000000..012ba20
--- /dev/null
+++ b/reference/exercises/concept/game-night/vendor/LeanTest/LeanTest.lean
@@ -0,0 +1,4 @@
+-- This module serves as the root of the `LeanTest` library.
+-- Import modules here that should be built as part of the library.
+import LeanTest.Assertions
+import LeanTest.Test
diff --git a/reference/exercises/concept/game-night/vendor/LeanTest/LeanTest/Assertions.lean b/reference/exercises/concept/game-night/vendor/LeanTest/LeanTest/Assertions.lean
new file mode 100644
index 0000000..60e4ad8
--- /dev/null
+++ b/reference/exercises/concept/game-night/vendor/LeanTest/LeanTest/Assertions.lean
@@ -0,0 +1,166 @@
+/-
+Assertion functions for unit testing.
+-/
+
+namespace LeanTest
+
+/-- Result of a test assertion -/
+inductive AssertionResult where
+  | success : AssertionResult
+  | failure (message : String) : AssertionResult
+  deriving Repr, BEq
+
+namespace AssertionResult
+
+def isSuccess : AssertionResult → Bool
+  | success => true
+  | failure _ => false
+
+def getMessage : AssertionResult → String
+  | success => "Assertion passed"
+  | failure msg => msg
+
+end AssertionResult
+
+/-- Assert that a boolean condition is true -/
+def assert (condition : Bool) (message : String := "Assertion failed") : AssertionResult :=
+  if condition then
+    .success
+  else
+    .failure message
+
+/-- Assert that two values are equal -/
+def assertEqual [BEq α] [Repr α] (expected : α) (actual : α) (message : String := "") : AssertionResult :=
+  if expected == actual then
+    .success
+  else
+    let msg := if message.isEmpty then
+      s!"Expected: {repr expected}\nActual: {repr actual}"
+    else
+      s!"{message}\nExpected: {repr expected}\nActual: {repr actual}"
+    .failure msg
+
+/-- Assert that two values are not equal -/
+def assertNotEqual [BEq α] [Repr α] (expected : α) (actual : α) (message : String := "") : AssertionResult :=
+  if expected != actual then
+    .success
+  else
+    let msg := if message.isEmpty then
+      s!"Expected values to be different, but both were: {repr expected}"
+    else
+      s!"{message}\nExpected values to be different, but both were: {repr expected}"
+    .failure msg
+
+/-- Refute that a boolean condition is true (assert it's false) -/
+def refute (condition : Bool) (message : String := "Refute failed - condition was true") : AssertionResult :=
+  if !condition then
+    .success
+  else
+    .failure message
+
+/-- Assert that a value is true -/
+def assertTrue (value : Bool) (message : String := "Expected true but got false") : AssertionResult :=
+  assert value message
+
+/-- Assert that a value is false -/
+def assertFalse (value : Bool) (message : String := "Expected false but got true") : AssertionResult :=
+  refute value message
+
+/-- Assert that an Option is some -/
+def assertSome [Repr α] (opt : Option α) (message : String := "Expected Some but got None") : AssertionResult :=
+  match opt with
+  | some _ => .success
+  | none => .failure message
+
+/-- Assert that an Option is none -/
+def assertNone [Repr α] (opt : Option α) (message : String := "") : AssertionResult :=
+  match opt with
+  | none => .success
+  | some val =>
+    let msg := if message.isEmpty then
+      s!"Expected None but got Some: {repr val}"
+    else
+      s!"{message}\nExpected None but got Some: {repr val}"
+    .failure msg
+
+/-- Assert that a list is empty -/
+def assertEmpty [Repr α] (list : List α) (message : String := "") : AssertionResult :=
+  match list with
+  | [] => .success
+  | _ =>
+    let msg := if message.isEmpty then
+      s!"Expected empty list but got: {repr list}"
+    else
+      s!"{message}\nExpected empty list but got: {repr list}"
+    .failure msg
+
+/-- Assert that a list contains an element -/
+def assertContains [BEq α] [Repr α] (list : List α) (element : α) (message : String := "") : AssertionResult :=
+  if list.contains element then
+    .success
+  else
+    let msg := if message.isEmpty then
+      s!"Expected list to contain {repr element}\nList: {repr list}"
+    else
+      s!"{message}\nExpected list to contain {repr element}\nList: {repr list}"
+    .failure msg
+
+/-- Assert that a value is within a range (inclusive) -/
+def assertInRange [LE α] [DecidableRel (· ≤ · : α → α → Prop)] [Repr α]
+    (value : α) (min : α) (max : α) (message : String := "") : AssertionResult :=
+  if min ≤ value ∧ value ≤ max then
+    .success
+  else
+    let msg := if message.isEmpty then
+      s!"Expected {repr value} to be in range [{repr min}, {repr max}]"
+    else
+      s!"{message}\nExpected {repr value} to be in range [{repr min}, {repr max}]"
+    .failure msg
+
+/-- Assert that an Except value is an error -/
+def assertError [Repr ε] [Repr α] (result : Except ε α) (message : String := "") : AssertionResult :=
+  match result with
+  | .error _ => .success
+  | .ok val =>
+    let msg := if message.isEmpty then
+      s!"Expected error but got Ok: {repr val}"
+    else
+      s!"{message}\nExpected error but got Ok: {repr val}"
+    .failure msg
+
+/-- Assert that an Except value is ok -/
+def assertOk [Repr ε] [Repr α] (result : Except ε α) (message : String := "") : AssertionResult :=
+  match result with
+  | .ok _ => .success
+  | .error err =>
+    let msg := if message.isEmpty then
+      s!"Expected Ok but got error: {repr err}"
+    else
+      s!"{message}\nExpected Ok but got error: {repr err}"
+    .failure msg
+
+/-- Assert that an IO action throws an error -/
+def assertThrows (action : IO α) (message : String := "") : IO AssertionResult := do
+  try
+    let _ ← action
+    let msg := if message.isEmpty then
+      "Expected IO action to throw an error, but it succeeded"
+    else
+      s!"{message}\nExpected IO action to throw an error, but it succeeded"
+    return .failure msg
+  catch _ =>
+    return .success
+
+/-- Assert that an IO action succeeds (doesn't throw) -/
+def assertSucceeds (action : IO α) (message : String := "") : IO AssertionResult := do
+  try
+    let _ ← action
+    return .success
+  catch e =>
+    let msg := if message.isEmpty then
+      s!"Expected IO action to succeed, but it threw: {e}"
+    else
+      s!"{message}\nExpected IO action to succeed, but it threw: {e}"
+    return .failure msg
+
+end LeanTest
diff --git a/reference/exercises/concept/game-night/vendor/LeanTest/LeanTest/Json.lean b/reference/exercises/concept/game-night/vendor/LeanTest/LeanTest/Json.lean
new file mode 100644
index 0000000..a61f6b9
--- /dev/null
+++ b/reference/exercises/concept/game-night/vendor/LeanTest/LeanTest/Json.lean
@@ -0,0 +1,57 @@
+/-
+Minimal, dependency-free JSON string building.
+-/
+
+namespace LeanTest.Json
+
+private def hexDigit (n : Nat) : Char :=
+  if n < 10 then Char.ofNat (n + 48) else Char.ofNat (n - 10 + 97)
+
+private def toHex4 (n : Nat) : String :=
+  let d0 := hexDigit ((n / 4096) % 16)
+  let d1 := hexDigit ((n / 256) % 16)
+  let d2 := hexDigit ((n / 16) % 16)
+  let d3 := hexDigit (n % 16)
+  String.ofList [d0, d1, d2, d3]
+
+private def escapeChar (c : Char) : String :=
+  match c with
+  | '"' => "\\\""
+  | '\\' => "\\\\"
+  | '\n' => "\\n"
+  | '\r' => "\\r"
+  | '\t' => "\\t"
+  | c => if c.toNat < 0x20 then "\\u" ++ toHex4 c.toNat else String.ofList [c]
+
+/-- Escape a string's contents for embedding between JSON double-quotes. -/
+def escape (s : String) : String :=
+  String.join (s.toList.map escapeChar)
+
+/-- A JSON string literal, including the surrounding quotes. -/
+def str (s : String) : String :=
+  "\"" ++ escape s ++ "\""
+
+/-- A JSON string literal, or `null` when absent. -/
+def strOrNull : Option String → String
+  | none => "null"
+  | some s => str s
+
+/-- A JSON number, or `null` when absent. -/
+def natOrNull : Option Nat → String
+  | none => "null"
+  | some n => toString n
+
+/-- Truncate `s` to at most `maxLen` characters. -/
+def truncate (s : String) (maxLen : Nat) : String :=
+  if s.length <= maxLen then s
+  else String.ofList (s.toList.take (maxLen - 1)) ++ "…"
+
+/-- Build a JSON object from a list of already-encoded `"key": value` pairs. -/
+def object (fields : List String) : String :=
+  "{" ++ String.intercalate ", " fields ++ "}"
+
+/-- Build a JSON array from a list of already-encoded elements. -/
+def array (elems : List String) : String :=
+  "[" ++ String.intercalate ", " elems ++ "]"
+
+end LeanTest.Json
diff --git a/reference/exercises/concept/game-night/vendor/LeanTest/LeanTest/SourceParser.lean b/reference/exercises/concept/game-night/vendor/LeanTest/LeanTest/SourceParser.lean
new file mode 100644
index 0000000..eaf5d23
--- /dev/null
+++ b/reference/exercises/concept/game-night/vendor/LeanTest/LeanTest/SourceParser.lean
@@ -0,0 +1,84 @@
+/-
+Extracts the literal source text of each `.addTest "<name>" (...)` call.
+-/
+
+namespace LeanTest.SourceParser
+
+private def listStartsWith : List Char → List Char → Bool
+  | _, [] => true
+  | [], _ :: _ => false
+  | x :: xs, p :: ps => x == p && listStartsWith xs ps
+
+private def isSpace (c : Char) : Bool :=
+  c == ' ' || c == '\t' || c == '\n' || c == '\r'
+
+/-- Trim leading/trailing whitespace. -/
+private def trimStr (s : String) : String :=
+  let chars := s.toList.dropWhile isSpace
+  String.ofList (chars.reverse.dropWhile isSpace).reverse
+
+/-- Return the remainder of the list after `marker`, or `none` if it doesn't occur. -/
+private partial def findMarker (xs : List Char) (marker : List Char) : Option (List Char) :=
+  match xs with
+  | [] => none
+  | _ :: rest =>
+    if listStartsWith xs marker then some (xs.drop marker.length)
+    else findMarker rest marker
+
+private partial def readStringLiteral (xs : List Char) : String × List Char :=
+  go xs #[]
+where
+  go (xs : List Char) (acc : Array Char) : String × List Char :=
+    match xs with
+    | [] => (String.ofList acc.toList, [])
+    | '\\' :: c :: rest => go rest (acc.push '\\' |>.push c)
+    | '"' :: rest => (String.ofList acc.toList, rest)
+    | c :: rest => go rest (acc.push c)
+
+private partial def readParenBody (xs : List Char) : String × List Char :=
+  match xs with
+  | '(' :: rest => go rest 0 #[] false
+  | _ => ("", xs)
+where
+  go (xs : List Char) (depth : Nat) (acc : Array Char) (inString : Bool) : String × List Char :=
+    match xs with
+    | [] => (String.ofList acc.toList, [])
+    | '\\' :: c :: rest =>
+      if inString then go rest depth (acc.push '\\' |>.push c) inString
+      else go (c :: rest) depth (acc.push '\\') inString
+    | '"' :: rest => go rest depth (acc.push '"') (!inString)
+    | '(' :: rest =>
+      if inString then go rest depth (acc.push '(') inString
+      else go rest (depth + 1) (acc.push '(') inString
+    | ')' :: rest =>
+      if inString then go rest depth (acc.push ')') inString
+      else if depth == 0 then (String.ofList acc.toList, rest)
+      else go rest (depth - 1) (acc.push ')') inString
+    | c :: rest => go rest depth (acc.push c) inString
+
+/-- Extract `(test name, source body)` pairs for each `.addTest "<name>" (...)` in `source`. -/
+partial def extractTestBodies (source : String) : List (String × String) :=
+  go source.toList #[]
+where
+  marker := ".addTest \"".toList
+  go (xs : List Char) (acc : Array (String × String)) : List (String × String) :=
+    match findMarker xs marker with
+    | none => acc.toList
+    | some afterMarker =>
+      let (name, afterName) := readStringLiteral afterMarker
+      let afterWs := afterName.dropWhile isSpace
+      let (body, rest) := readParenBody afterWs
+      let trimmed := (trimStr body).toList
+      let trimmed :=
+        if listStartsWith trimmed ['d', 'o'] then
+          (trimStr (String.ofList (trimmed.drop 2))).toList
+        else trimmed
+      go rest (acc.push (name, String.ofList trimmed))
+
+/-- Look up the captured source for `name`, or `""` if extraction found nothing. -/
+def lookup (name : String) (bodies : List (String × String)) : String :=
+  match bodies.find? (fun p => p.1 == name) with
+  | some (_, code) => code
+  | none => ""
+
+end LeanTest.SourceParser
diff --git a/reference/exercises/concept/game-night/vendor/LeanTest/LeanTest/Test.lean b/reference/exercises/concept/game-night/vendor/LeanTest/LeanTest/Test.lean
new file mode 100644
index 0000000..8e72377
--- /dev/null
+++ b/reference/exercises/concept/game-night/vendor/LeanTest/LeanTest/Test.lean
@@ -0,0 +1,198 @@
+/-
+Test case and test suite management.
+-/
+
+import LeanTest.Assertions
+import LeanTest.Json
+import LeanTest.SourceParser
+
+namespace LeanTest
+
+/-- A single test case -/
+structure TestCase where
+  description : String
+  test : IO AssertionResult
+  taskId : Option Nat := none -- set for concept exercises
+  deriving Inhabited
+
+/-- A collection of tests (test suite) -/
+structure TestSuite where
+  name : String
+  tests : List TestCase
+  deriving Inhabited
+
+namespace TestSuite
+
+/-- Create an empty test suite -/
+def empty (name : String) : TestSuite :=
+  { name := name, tests := [] }
+
+/-- Add a test to the suite -/
+def addTest (suite : TestSuite) (description : String) (test : IO AssertionResult)
+    (taskId : Option Nat := none) : TestSuite :=
+  { suite with tests := suite.tests ++ [{ description := description, test := test, taskId := taskId }] }
+
+end TestSuite
+
+/-- Per-test outcome, matching the v3 interface's `pass` / `fail` / `error`. -/
+inductive TestStatus where
+  | pass
+  | fail
+  | error
+  deriving Repr, BEq
+
+def TestStatus.toReportString : TestStatus → String
+  | .pass => "pass"
+  | .fail => "fail"
+  | .error => "error"
+
+/-- Result of running a test -/
+structure TestResult where
+  description : String
+  status : TestStatus
+  message : Option String -- `none` when `status = .pass`
+  taskId : Option Nat
+  deriving Repr
+
+/-- Test statistics -/
+structure TestStats where
+  total : Nat := 0
+  passed : Nat := 0
+  failed : Nat := 0
+  errored : Nat := 0
+
+namespace TestStats
+
+def empty : TestStats := {}
+
+def addResult (stats : TestStats) (status : TestStatus) : TestStats :=
+  { stats with
+    total := stats.total + 1
+    passed := stats.passed + (if status == .pass then 1 else 0)
+    failed := stats.failed + (if status == .fail then 1 else 0)
+    errored := stats.errored + (if status == .error then 1 else 0) }
+
+end TestStats
+
+/-- ANSI color codes for terminal output -/
+def greenColor : String := "\x1b[32m"
+def redColor : String := "\x1b[31m"
+def yellowColor : String := "\x1b[33m"
+def resetColor : String := "\x1b[0m"
+def boldColor : String := "\x1b[1m"
+
+/-- Run a single test, printing a colored result line, and returning a structured `TestResult`.
+    Exceptions are caught and returned as a per-test `error`. -/
+def runTest (testCase : TestCase) : IO TestResult := do
+  try
+    let result ← testCase.test
+    match result with
+    | .success =>
+      IO.println s!"  {greenColor}✓{resetColor} {testCase.description}"
+      return { description := testCase.description, status := .pass, message := none, taskId := testCase.taskId }
+    | .failure msg =>
+      IO.println s!"  {redColor}✗{resetColor} {testCase.description}"
+      IO.println s!"    {redColor}{msg}{resetColor}"
+      return { description := testCase.description, status := .fail, message := some msg, taskId := testCase.taskId }
+  catch e =>
+    let msg := toString e
+    IO.println s!"  {redColor}✗{resetColor} {testCase.description}"
+    IO.println s!"    {redColor}{msg}{resetColor}"
+    return { description := testCase.description, status := .error, message := some msg, taskId := testCase.taskId }
+
+/-- Run all tests in a test suite -/
+def runTestSuite (suite : TestSuite) : IO (List TestResult) := do
+  IO.println s!"\n{boldColor}{suite.name}{resetColor}"
+  let mut results : List TestResult := []
+  for testCase in suite.tests do
+    let result ← runTest testCase
+    results := results ++ [result]
+  return results
+
+/-- Print test summary -/
+def printSummary (stats : TestStats) : IO Unit := do
+  IO.println ""
+  IO.println s!"{boldColor}Test Summary:{resetColor}"
+  IO.println s!"  Total:  {stats.total}"
+  IO.println s!"  {greenColor}Passed: {stats.passed}{resetColor}"
+
+  if stats.failed > 0 then
+    IO.println s!"  {redColor}Failed: {stats.failed}{resetColor}"
+  if stats.errored > 0 then
+    IO.println s!"  {redColor}Errored: {stats.errored}{resetColor}"
+
+  if stats.failed > 0 || stats.errored > 0 then
+    IO.println s!"\n{redColor}FAILED{resetColor}"
+  else
+    IO.println s!"\n{greenColor}ALL TESTS PASSED{resetColor}"
+
+/-- Build the v3 `results.json` payload for a full run's `TestResult`s.
+    `testCode` maps each test's description to its captured source.
+    `results` may be empty if an exercise is compile-time only (theorem proving, etc.). -/
+def buildResultsJson (results : List TestResult) (testCode : List (String × String)) : String :=
+  open Json in
+  let overall : TestStatus :=
+    if results.all (fun t => t.status == .pass) then .pass
+    else if !results.isEmpty && results.all (fun t => t.status == .error) then .error
+    else .fail
+  let testJson (t : TestResult) : String :=
+    let code := SourceParser.lookup t.description testCode
+    let fields :=
+      [ s!"\"name\": {str t.description}"
+      , s!"\"status\": {str t.status.toReportString}"
+      , s!"\"message\": {strOrNull t.message}"
+      , s!"\"test_code\": {str code}"
+      ] ++ (match t.taskId with
+            | none => []
+            | some n => [s!"\"task_id\": {n}"])
+    object fields
+  let topMessage : Option String :=
+    match overall with
+    | .error =>
+      let firstMsg := results.head?.bind (·.message)
+      some (truncate (firstMsg.getD "All tests failed with an error.") 65535)
+    | _ => none
+  object [
+    s!"\"version\": 3",
+    s!"\"status\": {str overall.toReportString}",
+    s!"\"message\": {strOrNull topMessage}",
+    s!"\"tests\": {array (results.map testJson)}"
+  ]
+
+/-- If the runner set `EXERCISM_OUTPUT_DIR`, write `results.json` there.
+    Reads `EXERCISM_TEST_FILE` (if set) to source `test_code` from the test file.
+    Silently does nothing when `EXERCISM_OUTPUT_DIR` is unset. -/
+def writeResultsIfRequested (results : List TestResult) : IO Unit := do
+  match (← IO.getEnv "EXERCISM_OUTPUT_DIR") with
+  | none => pure ()
+  | some outputDir =>
+    let testCode ←
+      match (← IO.getEnv "EXERCISM_TEST_FILE") with
+      | none => pure []
+      | some path =>
+        try
+          let source ← IO.FS.readFile path
+          pure (SourceParser.extractTestBodies source)
+        catch _ => pure []
+    IO.FS.createDirAll outputDir
+    IO.FS.writeFile s!"{outputDir}/results.json" (buildResultsJson results testCode)
+
+/-- Run multiple test suites, print a summary.
+    If the proper env vars are set, write `results.json`. -/
+def runTestSuites (suites : List TestSuite) : IO (List TestResult) := do
+  let mut allResults : List TestResult := []
+  for suite in suites do
+    let results ← runTestSuite suite
+    allResults := allResults ++ results
+
+  let stats := allResults.foldl (fun s r => s.addResult r.status) TestStats.empty
+  printSummary stats
+  writeResultsIfRequested allResults
+  return allResults
+
+/-- Run multiple test suites and return exit code (0 = all passed, 1 = some failed/errored) -/
+def runTestSuitesWithExitCode (suites : List TestSuite) : IO UInt32 := do
+  let results ← runTestSuites suites
+  return if results.any (fun r => r.status != .pass) then 1 else 0
+
+end LeanTest
diff --git a/reference/exercises/concept/mountain-hike/MountainHike.lean b/reference/exercises/concept/mountain-hike/MountainHike.lean
index d5f2808..93c163a 100644
--- a/reference/exercises/concept/mountain-hike/MountainHike.lean
+++ b/reference/exercises/concept/mountain-hike/MountainHike.lean
@@ -1,13 +1,18 @@
 namespace MountainHike
 
-def totalMinutes (hours minutes : Nat) : Nat := sorry --remove this line and implement the function
+def totalMinutes (hours minutes : Nat) : Nat :=
+  sorry --remove this line and implement the function
 
-def fullHours (totalMinutes : Nat) : Nat := sorry --remove this line and implement the function
+def fullHours (totalMinutes : Nat) : Nat :=
+  sorry --remove this line and implement the function
 
-def remainingMinutes (totalMinutes : Nat) : Nat := sorry --remove this line and implement the function
+def remainingMinutes (totalMinutes : Nat) : Nat :=
+  sorry --remove this line and implement the function
 
-def waterLeft (capacity used : Nat) : Nat := sorry --remove this line and implement the function
+def waterLeft (capacity used : Nat) : Nat :=
+  sorry --remove this line and implement the function
 
-def elevationChange (beginAlt endAlt : Int) : Int := sorry --remove this line and implement the function
+def elevationChange (beginAlt endAlt : Int) : Int :=
+  sorry --remove this line and implement the function
 
 end MountainHike