diff --git a/config.json b/config.json
index 09e3b85..0e40e01 100644
--- a/config.json
+++ b/config.json
@@ -722,6 +722,14 @@
         "prerequisites": [],
         "difficulty": 8
       },
+      {
+        "slug": "alphametics",
+        "name": "Alphametics",
+        "uuid": "ac086674-808b-4f36-be70-725174f1caff",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 8
+      },
       {
         "slug": "bank-account",
         "name": "Bank Account",
diff --git a/exercises/practice/alphametics/.docs/instructions.md b/exercises/practice/alphametics/.docs/instructions.md
new file mode 100644
index 0000000..ef2cbb4
--- /dev/null
+++ b/exercises/practice/alphametics/.docs/instructions.md
@@ -0,0 +1,29 @@
+# Instructions
+
+Given an alphametics puzzle, find the correct solution.
+
+[Alphametics][alphametics] is a puzzle where letters in words are replaced with numbers.
+
+For example `SEND + MORE = MONEY`:
+
+```text
+  S E N D
+  M O R E +
+-----------
+M O N E Y
+```
+
+Replacing these with valid numbers gives:
+
+```text
+  9 5 6 7
+  1 0 8 5 +
+-----------
+1 0 6 5 2
+```
+
+This is correct because every letter is replaced by a different number and the words, translated into numbers, then make a valid sum.
+
+Each letter must represent a different digit, and the leading digit of a multi-digit number must not be zero.
+
+[alphametics]: https://en.wikipedia.org/wiki/Alphametics
diff --git a/exercises/practice/alphametics/.meta/Example.lean b/exercises/practice/alphametics/.meta/Example.lean
new file mode 100644
index 0000000..ddd64ec
--- /dev/null
+++ b/exercises/practice/alphametics/.meta/Example.lean
@@ -0,0 +1,82 @@
+namespace Alphametics
+
+private structure Letter where
+  ch : Char
+  leading : Nat
+  rank : Nat
+  weight : Array Int
+
+private def wordSigns (tokens : List String) : List (String × Int) := Id.run do
+  let mut sign : Int := -1
+  let mut result : List (String × Int) := []
+  for tok in tokens do
+    if tok == "==" then
+      sign := 1
+    else if tok != "+" then
+      result := (tok, sign) :: result
+  return result
+
+private def uniqueLetters (puzzle : String) : List Char :=
+  puzzle.toList.filter Char.isAlpha
+    |>.foldl (fun acc c => if acc.contains c then acc else c :: acc) []
+
+private def makeLetter (words : List (String × Int)) (numCols : Nat) (ch : Char) : Letter := Id.run do
+  let mut weight : Array Int := Array.replicate numCols 0
+  let mut leading : Nat := 0
+  for (word, sign) in words do
+    let chars := word.toList.toArray
+    let len := chars.size
+    if len > 1 && chars[0]! == ch then
+      leading := 1
+    for i in [:len] do
+      if chars[len - 1 - i]! == ch then
+        weight := weight.set! i (weight[i]! + sign)
+  let rank :=
+    (List.range numCols).find? (fun col => weight[col]! != 0)
+      |>.getD (numCols - 1)
+  return { ch, leading, rank, weight }
+
+private def columnSum (letters : List Letter) (mapping : List (Char × Nat)) (col : Nat) : Int :=
+  letters.foldl (fun acc l =>
+    acc + l.weight[col]! * (Int.ofNat (mapping.lookup l.ch |>.getD 0))) 0
+
+-- Depth-first search. `remaining` holds letters not yet assigned,
+-- sorted by rank ascending; `col` is the current column (0 = rightmost).
+-- When the next letter's rank exceeds `col`, validate the column sum
+-- (accounting for `carry`) and advance to the next column.
+private partial def search (numCols : Nat) (allLetters : List Letter)
+    (col : Nat) (carry : Int) (remaining : List Letter) (claimed : Nat)
+    (mapping : List (Char × Nat)) : Option (List (Char × Nat)) :=
+  let columnComplete : Bool :=
+    match remaining with
+    | [] => true
+    | entry :: _ => entry.rank > col
+  if columnComplete then
+    let colSum := carry + columnSum allLetters mapping col
+    if colSum % 10 != 0 then
+      none
+    else if col + 1 < numCols then
+      search numCols allLetters (col + 1) (colSum / 10) remaining claimed mapping
+    else if colSum == 0 then
+      some (mapping.mergeSort (fun a b => a.1 ≤ b.1))
+    else
+      none
+  else
+    match remaining with
+    | [] => none
+    | entry :: rest =>
+      ((List.range 10).filter (· ≥ entry.leading)).findSome? (fun digit =>
+        if claimed &&& (1 <<< digit) == 0 then
+          search numCols allLetters col carry rest
+            (claimed ||| (1 <<< digit)) ((entry.ch, digit) :: mapping)
+        else
+          none)
+
+def solve (puzzle : String) : Option (List (Char × Nat)) :=
+  let words := wordSigns ((puzzle.splitOn " ").filter (· != ""))
+  let numCols := (words.map (fun (w, _) => w.length)).foldl max 0
+  let uniq := uniqueLetters puzzle
+  let allLetters := (uniq.map (makeLetter words numCols)).mergeSort (fun a b => a.rank ≤ b.rank)
+  search numCols allLetters 0 0 allLetters 0 []
+
+end Alphametics
diff --git a/exercises/practice/alphametics/.meta/config.json b/exercises/practice/alphametics/.meta/config.json
new file mode 100644
index 0000000..4b05e9b
--- /dev/null
+++ b/exercises/practice/alphametics/.meta/config.json
@@ -0,0 +1,17 @@
+{
+  "authors": [
+    "keiravillekode"
+  ],
+  "files": {
+    "solution": [
+      "Alphametics.lean"
+    ],
+    "test": [
+      "AlphameticsTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Given an alphametics puzzle, find the correct solution."
+}
diff --git a/exercises/practice/alphametics/.meta/extra.json b/exercises/practice/alphametics/.meta/extra.json
new file mode 100644
index 0000000..a2036bf
--- /dev/null
+++ b/exercises/practice/alphametics/.meta/extra.json
@@ -0,0 +1,20 @@
+[
+  {
+    "description": "puzzle with a colors theme",
+    "property": "solve",
+    "input": {
+      "puzzle": "GREEN + ORANGE == COLORS"
+    },
+    "expected": {
+      "A": 5,
+      "C": 2,
+      "E": 4,
+      "G": 8,
+      "L": 9,
+      "N": 6,
+      "O": 1,
+      "R": 3,
+      "S": 0
+    }
+  }
+]
diff --git a/exercises/practice/alphametics/.meta/tests.toml b/exercises/practice/alphametics/.meta/tests.toml
new file mode 100644
index 0000000..f599b3d
--- /dev/null
+++ b/exercises/practice/alphametics/.meta/tests.toml
@@ -0,0 +1,40 @@
+# This is an auto-generated file.
+#
+# Regenerating this file via `configlet sync` will:
+# - Recreate every `description` key/value pair
+# - Recreate every `reimplements` key/value pair, where they exist in problem-specifications
+# - Remove any `include = true` key/value pair (an omitted `include` key implies inclusion)
+# - Preserve any other key/value pair
+#
+# As user-added comments (using the # character) will be removed when this file
+# is regenerated, comments can be added via a `comment` key.
+
+[e0c08b07-9028-4d5f-91e1-d178fead8e1a]
+description = "puzzle with three letters"
+
+[a504ee41-cb92-4ec2-9f11-c37e95ab3f25]
+description = "solution must have unique value for each letter"
+
+[4e3b81d2-be7b-4c5c-9a80-cd72bc6d465a]
+description = "leading zero solution is invalid"
+
+[8a3e3168-d1ee-4df7-94c7-b9c54845ac3a]
+description = "puzzle with two digits final carry"
+
+[a9630645-15bd-48b6-a61e-d85c4021cc09]
+description = "puzzle with four letters"
+
+[3d905a86-5a52-4e4e-bf80-8951535791bd]
+description = "puzzle with six letters"
+
+[4febca56-e7b7-4789-97b9-530d09ba95f0]
+description = "puzzle with seven letters"
+
+[12125a75-7284-4f9a-a5fa-191471e0d44f]
+description = "puzzle with eight letters"
+
+[fb05955f-38dc-477a-a0b6-5ef78969fffa]
+description = "puzzle with ten letters"
+
+[9a101e81-9216-472b-b458-b513a7adacf7]
+description = "puzzle with ten letters and 199 addends"
diff --git a/exercises/practice/alphametics/Alphametics.lean b/exercises/practice/alphametics/Alphametics.lean
new file mode 100644
index 0000000..9aa8e64
--- /dev/null
+++ b/exercises/practice/alphametics/Alphametics.lean
@@ -0,0 +1,6 @@
+namespace Alphametics
+
+def solve (puzzle : String) : Option (List (Char × Nat)) :=
+  sorry --remove this line and implement the function
+
+end Alphametics
diff --git a/exercises/practice/alphametics/AlphameticsTest.lean b/exercises/practice/alphametics/AlphameticsTest.lean
new file mode 100644
index 0000000..1000e7a
--- /dev/null
+++ b/exercises/practice/alphametics/AlphameticsTest.lean
@@ -0,0 +1,43 @@
+import LeanTest
+import Alphametics
+
+open LeanTest
+
+def alphameticsTests : TestSuite :=
+  (TestSuite.empty "Alphametics")
+  |>.addTest "puzzle with three letters" (do
+      return assertEqual (some [('B', 9), ('I', 1), ('L', 0)])
+          (Alphametics.solve "I + BB == ILL"))
+  |>.addTest "solution must have unique value for each letter" (do
+      return assertEqual none
+          (Alphametics.solve "A == B"))
+  |>.addTest "leading zero solution is invalid" (do
+      return assertEqual none
+          (Alphametics.solve "ACA + DD == BD"))
+  |>.addTest "puzzle with two digits final carry" (do
+      return assertEqual (some [('A', 9), ('B', 1), ('C', 0)])
+          (Alphametics.solve "A + A + A + A + A + A + A + A + A + A + A + B == BCC"))
+  |>.addTest "puzzle with four letters" (do
+      return assertEqual (some [('A', 9), ('M', 1), ('O', 0), ('S', 2)])
+          (Alphametics.solve "AS + A == MOM"))
+  |>.addTest "puzzle with six letters" (do
+      return assertEqual (some [('A', 0), ('E', 2), ('L', 1), ('N', 7), ('O', 4), ('T', 9)])
+          (Alphametics.solve "NO + NO + TOO == LATE"))
+  |>.addTest "puzzle with seven letters" (do
+      return assertEqual (some [('E', 4), ('G', 2), ('H', 5), ('I', 0), ('L', 1), ('S', 9), ('T', 7)])
+          (Alphametics.solve "HE + SEES + THE == LIGHT"))
+  |>.addTest "puzzle with eight letters" (do
+      return assertEqual (some [('D', 7), ('E', 5), ('M', 1), ('N', 6), ('O', 0), ('R', 8), ('S', 9), ('Y', 2)])
+          (Alphametics.solve "SEND + MORE == MONEY"))
+  |>.addTest "puzzle with ten letters" (do
+      return assertEqual (some [('A', 5), ('D', 3), ('E', 4), ('F', 7), ('G', 8), ('N', 0), ('O', 2), ('R', 1), ('S', 6), ('T', 9)])
+          (Alphametics.solve "AND + A + STRONG + OFFENSE + AS + A + GOOD == DEFENSE"))
+  |>.addTest "puzzle with ten letters and 199 addends" (do
+      return assertEqual (some [('A', 1), ('E', 0), ('F', 5), ('H', 8), ('I', 7), ('L', 2), ('O', 6), ('R', 3), ('S', 4), ('T', 9)])
+          (Alphametics.solve "THIS + A + FIRE + THEREFORE + FOR + ALL + HISTORIES + I + TELL + A + TALE + THAT + FALSIFIES + ITS + TITLE + TIS + A + LIE + THE + TALE + OF + THE + LAST + FIRE + HORSES + LATE + AFTER + THE + FIRST + FATHERS + FORESEE + THE + HORRORS + THE + LAST + FREE + TROLL + TERRIFIES + THE + HORSES + OF + FIRE + THE + TROLL + RESTS + AT + THE + HOLE + OF + LOSSES + IT + IS + THERE + THAT + SHE + STORES + ROLES + OF + LEATHERS + AFTER + SHE + SATISFIES + HER + HATE + OFF + THOSE + FEARS + A + TASTE + RISES + AS + SHE + HEARS + THE + LEAST + FAR + HORSE + THOSE + FAST + HORSES + THAT + FIRST + HEAR + THE + TROLL + FLEE + OFF + TO + THE + FOREST + THE + HORSES + THAT + ALERTS + RAISE + THE + STARES + OF + THE + OTHERS + AS + THE + TROLL + ASSAILS + AT + THE + TOTAL + SHIFT + HER + TEETH + TEAR + HOOF + OFF + TORSO + AS + THE + LAST + HORSE + FORFEITS + ITS + LIFE + THE + FIRST + FATHERS + HEAR + OF + THE + HORRORS + THEIR + FEARS + THAT + THE + FIRES + FOR + THEIR + FEASTS + ARREST + AS + THE + FIRST + FATHERS + RESETTLE + THE + LAST + OF + THE + FIRE + HORSES + THE + LAST + TROLL + HARASSES + THE + FOREST + HEART + FREE + AT + LAST + OF + THE + LAST + TROLL + ALL + OFFER + THEIR + FIRE + HEAT + TO + THE + ASSISTERS + FAR + OFF + THE + TROLL + FASTS + ITS + LIFE + SHORTER + AS + STARS + RISE + THE + HORSES + REST + SAFE + AFTER + ALL + SHARE + HOT + FISH + AS + THEIR + AFFILIATES + TAILOR + A + ROOFS + FOR + THEIR + SAFE == FORTRESSES"))
+  |>.addTest "puzzle with a colors theme" (do
+      return assertEqual (some [('A', 5), ('C', 2), ('E', 4), ('G', 8), ('L', 9), ('N', 6), ('O', 1), ('R', 3), ('S', 0)])
+          (Alphametics.solve "GREEN + ORANGE == COLORS"))
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [alphameticsTests]
diff --git a/exercises/practice/alphametics/lakefile.toml b/exercises/practice/alphametics/lakefile.toml
new file mode 100644
index 0000000..3675329
--- /dev/null
+++ b/exercises/practice/alphametics/lakefile.toml
@@ -0,0 +1,15 @@
+name = "alphametics"
+version = "0.1.0"
+defaultTargets = ["AlphameticsTest"]
+testDriver = "AlphameticsTest"
+
+[[lean_lib]]
+name = "LeanTest"
+srcDir = "vendor/LeanTest"
+
+[[lean_lib]]
+name = "Alphametics"
+
+[[lean_exe]]
+name = "AlphameticsTest"
+root = "AlphameticsTest"
diff --git a/exercises/practice/alphametics/lean-toolchain b/exercises/practice/alphametics/lean-toolchain
new file mode 100644
index 0000000..14791d7
--- /dev/null
+++ b/exercises/practice/alphametics/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.29.0
diff --git a/exercises/practice/alphametics/vendor/LeanTest/LeanTest.lean b/exercises/practice/alphametics/vendor/LeanTest/LeanTest.lean
new file mode 100644
index 0000000..012ba20
--- /dev/null
+++ b/exercises/practice/alphametics/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/exercises/practice/alphametics/vendor/LeanTest/LeanTest/Assertions.lean b/exercises/practice/alphametics/vendor/LeanTest/LeanTest/Assertions.lean
new file mode 100644
index 0000000..60e4ad8
--- /dev/null
+++ b/exercises/practice/alphametics/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/exercises/practice/alphametics/vendor/LeanTest/LeanTest/Test.lean b/exercises/practice/alphametics/vendor/LeanTest/LeanTest/Test.lean
new file mode 100644
index 0000000..5ddbae5
--- /dev/null
+++ b/exercises/practice/alphametics/vendor/LeanTest/LeanTest/Test.lean
@@ -0,0 +1,130 @@
+/-
+Test case and test suite management.
+-/
+
+import LeanTest.Assertions
+
+namespace LeanTest
+
+/-- A single test case -/
+structure TestCase where
+  description : String
+  test : IO AssertionResult
+  deriving Inhabited
+
+/-- Result of running a test -/
+structure TestResult where
+  description : String
+  result : AssertionResult
+  deriving Repr
+
+/-- 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) : TestSuite :=
+  { suite with tests := suite.tests ++ [{ description := description, test := test }] }
+
+end TestSuite
+
+/-- Test statistics -/
+structure TestStats where
+  total : Nat
+  passed : Nat
+  failed : Nat
+  deriving Repr
+
+namespace TestStats
+
+def empty : TestStats :=
+  { total := 0, passed := 0, failed := 0 }
+
+def addResult (stats : TestStats) (result : AssertionResult) : TestStats :=
+  { total := stats.total + 1
+  , passed := if result.isSuccess then stats.passed + 1 else stats.passed
+  , failed := if result.isSuccess then stats.failed else stats.failed + 1
+  }
+
+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 and print the result -/
+def runTest (testCase : TestCase) : IO TestResult := do
+  let result ← testCase.test
+  match result with
+  | .success =>
+    IO.println s!"  {greenColor}✓{resetColor} {testCase.description}"
+  | .failure msg =>
+    IO.println s!"  {redColor}✗{resetColor} {testCase.description}"
+    IO.println s!"    {redColor}{msg}{resetColor}"
+  return { description := testCase.description, result := result }
+
+/-- Run all tests in a test suite -/
+def runTestSuite (suite : TestSuite) : IO TestStats := do
+  IO.println s!"\n{boldColor}{suite.name}{resetColor}"
+  let mut stats := TestStats.empty
+
+  for testCase in suite.tests do
+    let result ← runTest testCase
+    stats := stats.addResult result.result
+
+  return stats
+
+/-- 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}"
+    IO.println s!"\n{redColor}FAILED{resetColor}"
+  else
+    IO.println s!"\n{greenColor}ALL TESTS PASSED{resetColor}"
+
+/-- Run multiple test suites -/
+def runTestSuites (suites : List TestSuite) : IO Unit := do
+  let mut totalStats := TestStats.empty
+
+  for suite in suites do
+    let stats ← runTestSuite suite
+    totalStats := {
+      total := totalStats.total + stats.total,
+      passed := totalStats.passed + stats.passed,
+      failed := totalStats.failed + stats.failed
+    }
+
+  printSummary totalStats
+
+/-- Run multiple test suites and return exit code (0 = all passed, 1 = some failed) -/
+def runTestSuitesWithExitCode (suites : List TestSuite) : IO UInt32 := do
+  let mut totalStats := TestStats.empty
+
+  for suite in suites do
+    let stats ← runTestSuite suite
+    totalStats := {
+      total := totalStats.total + stats.total,
+      passed := totalStats.passed + stats.passed,
+      failed := totalStats.failed + stats.failed
+    }
+
+  printSummary totalStats
+  return if totalStats.failed > 0 then 1 else 0
+
+end LeanTest
diff --git a/generators/Generator/Generator.lean b/generators/Generator/Generator.lean
index 527d9d4..bfb905d 100644
--- a/generators/Generator/Generator.lean
+++ b/generators/Generator/Generator.lean
@@ -1,3 +1,4 @@
+import Generator.AlphameticsGenerator
 import Generator.PascalsTriangleGenerator
 import Generator.ResistorColorDuoGenerator
 import Generator.VariableLengthQuantityGenerator
@@ -106,6 +107,7 @@ abbrev endBodyGenerator := String -> String
 
 def dispatch : Std.HashMap String (introGenerator × testCaseGenerator × endBodyGenerator) :=
   Std.HashMap.ofList [
+    ("Alphametics", (AlphameticsGenerator.genIntro, AlphameticsGenerator.genTestCase, AlphameticsGenerator.genEnd)),
     ("PascalsTriangle", (PascalsTriangleGenerator.genIntro, PascalsTriangleGenerator.genTestCase, PascalsTriangleGenerator.genEnd)),
     ("ResistorColorDuo", (ResistorColorDuoGenerator.genIntro, ResistorColorDuoGenerator.genTestCase, ResistorColorDuoGenerator.genEnd)),
     ("VariableLengthQuantity", (VariableLengthQuantityGenerator.genIntro, VariableLengthQuantityGenerator.genTestCase, VariableLengthQuantityGenerator.genEnd)),
diff --git a/generators/Generator/Generator/AlphameticsGenerator.lean b/generators/Generator/Generator/AlphameticsGenerator.lean
new file mode 100644
index 0000000..1d8a72e
--- /dev/null
+++ b/generators/Generator/Generator/AlphameticsGenerator.lean
@@ -0,0 +1,52 @@
+import Lean.Data.Json
+import Std
+import Helper
+
+open Lean
+open Std
+open Helper
+
+namespace AlphameticsGenerator
+
+def genIntro (exercise : String) : String := s!"import LeanTest
+import {exercise}
+
+open LeanTest
+
+def {exercise.decapitalize}Tests : TestSuite :=
+  (TestSuite.empty \"{exercise}\")"
+
+-- Canonical data's `expected` is either `null` (no solution) or an
+-- object like `{\"I\": 1, \"B\": 9, \"L\": 0}`. We render as
+-- `none` or `(some [('B', 9), ('I', 1), ('L', 0)])`; keys are read out
+-- of the JSON object in RBNode order, which is alphabetical by string,
+-- matching what Example.lean's `solve` produces.
+def renderExpected (expected : Json) : String :=
+  if expected.isNull then
+    "none"
+  else
+    let pairs := getOk expected.getObj?
+                  |>.toList
+                  |>.map (fun (k, v) => s!"('{k.toList.head!}', {v})")
+                  |> String.intercalate ", "
+    s!"(some [{pairs}])"
+
+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})"
+  s!"
+  |>.addTest {description} (do
+      return assertEqual {renderExpected expected}\n          {call})"
+
+def genEnd (exercise : String) : String :=
+  s!"
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [{exercise.decapitalize}Tests]
+"
+
+end AlphameticsGenerator