diff --git a/config.json b/config.json
index 5876362..09e3b85 100644
--- a/config.json
+++ b/config.json
@@ -634,6 +634,14 @@
         "prerequisites": [],
         "difficulty": 6
       },
+      {
+        "slug": "pascals-triangle",
+        "name": "Pascal's Triangle",
+        "uuid": "d37330c0-a6b9-4e24-b28d-0d4b1b2b35b0",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 6
+      },
       {
         "slug": "rail-fence-cipher",
         "name": "Rail Fence Cipher",
diff --git a/exercises/practice/pascals-triangle/.docs/instructions.md b/exercises/practice/pascals-triangle/.docs/instructions.md
new file mode 100644
index 0000000..0f58f00
--- /dev/null
+++ b/exercises/practice/pascals-triangle/.docs/instructions.md
@@ -0,0 +1,35 @@
+# Instructions
+
+Your task is to output the first N rows of Pascal's triangle.
+
+[Pascal's triangle][wikipedia] is a triangular array of positive integers.
+
+In Pascal's triangle, the number of values in a row is equal to its row number (which starts at one).
+Therefore, the first row has one value, the second row has two values, and so on.
+
+The first (topmost) row has a single value: `1`.
+Subsequent rows' values are computed by adding the numbers directly to the right and left of the current position in the previous row.
+
+If the previous row does _not_ have a value to the left or right of the current position (which only happens for the leftmost and rightmost positions), treat that position's value as zero (effectively "ignoring" it in the summation).
+
+## Example
+
+Let's look at the first 5 rows of Pascal's Triangle:
+
+```text
+    1
+   1 1
+  1 2 1
+ 1 3 3 1
+1 4 6 4 1
+```
+
+The topmost row has one value, which is `1`.
+
+The leftmost and rightmost values have only one preceding position to consider, which is the position to its right respectively to its left.
+With the topmost value being `1`, it follows from this that all the leftmost and rightmost values are also `1`.
+
+The other values all have two positions to consider.
+For example, the fifth row's (`1 4 6 4 1`) middle value is `6`, as the values to its left and right in the preceding row are `3` and `3`:
+
+[wikipedia]: https://en.wikipedia.org/wiki/Pascal%27s_triangle
diff --git a/exercises/practice/pascals-triangle/.docs/introduction.md b/exercises/practice/pascals-triangle/.docs/introduction.md
new file mode 100644
index 0000000..eab454e
--- /dev/null
+++ b/exercises/practice/pascals-triangle/.docs/introduction.md
@@ -0,0 +1,22 @@
+# Introduction
+
+With the weather being great, you're not looking forward to spending an hour in a classroom.
+Annoyed, you enter the class room, where you notice a strangely satisfying triangle shape on the blackboard.
+Whilst waiting for your math teacher to arrive, you can't help but notice some patterns in the triangle: the outer values are all ones, each subsequent row has one more value than its previous row and the triangle is symmetrical.
+Weird!
+
+Not long after you sit down, your teacher enters the room and explains that this triangle is the famous [Pascal's triangle][wikipedia].
+
+Over the next hour, your teacher reveals some amazing things hidden in this triangle:
+
+- It can be used to compute how many ways you can pick K elements from N values.
+- It contains the Fibonacci sequence.
+- If you color odd and even numbers differently, you get a beautiful pattern called the [Sierpiński triangle][wikipedia-sierpinski-triangle].
+
+The teacher implores you and your classmates to look up other uses, and assures you that there are lots more!
+At that moment, the school bell rings.
+You realize that for the past hour, you were completely absorbed in learning about Pascal's triangle.
+You quickly grab your laptop from your bag and go outside, ready to enjoy both the sunshine _and_ the wonders of Pascal's triangle.
+
+[wikipedia]: https://en.wikipedia.org/wiki/Pascal%27s_triangle
+[wikipedia-sierpinski-triangle]: https://en.wikipedia.org/wiki/Sierpi%C5%84ski_triangle
diff --git a/exercises/practice/pascals-triangle/.meta/Example.lean b/exercises/practice/pascals-triangle/.meta/Example.lean
new file mode 100644
index 0000000..84008bb
--- /dev/null
+++ b/exercises/practice/pascals-triangle/.meta/Example.lean
@@ -0,0 +1,23 @@
+namespace PascalsTriangle
+
+structure Triangle where
+  private mk ::
+  rows : IO.Ref (Array (Array Nat))
+
+def mkTriangle : IO Triangle := do
+  return {
+    rows := ← IO.mkRef #[ #[], #[1] ]
+  }
+
+private def buildRows (triangle : Triangle) (n : Nat) : IO (Array Nat) := do
+  let mut crt ← triangle.rows.get
+  while n ≥ crt.size do
+    let last := crt.back!
+    let next := (#[0] ++ last).zipWith (· + ·) (last.push 0)
+    crt := crt.push next
+  triangle.rows.set crt
+  return crt[n]!
+
+end PascalsTriangle
+
+notation triangle "(" n ")" => PascalsTriangle.buildRows triangle n
diff --git a/exercises/practice/pascals-triangle/.meta/config.json b/exercises/practice/pascals-triangle/.meta/config.json
new file mode 100644
index 0000000..f31ef63
--- /dev/null
+++ b/exercises/practice/pascals-triangle/.meta/config.json
@@ -0,0 +1,19 @@
+{
+  "authors": [
+    "oxe-i"
+  ],
+  "files": {
+    "solution": [
+      "PascalsTriangle.lean"
+    ],
+    "test": [
+      "PascalsTriangleTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Compute Pascal's triangle up to a given number of rows.",
+  "source": "Pascal's Triangle at Wolfram Math World",
+  "source_url": "https://www.wolframalpha.com/input/?i=Pascal%27s+triangle"
+}
diff --git a/exercises/practice/pascals-triangle/.meta/extra.json b/exercises/practice/pascals-triangle/.meta/extra.json
new file mode 100644
index 0000000..263dcf6
--- /dev/null
+++ b/exercises/practice/pascals-triangle/.meta/extra.json
@@ -0,0 +1,18 @@
+[
+  {
+    "description": "big row",
+    "property": "property",
+    "input": {
+      "count": 100
+    },
+    "expected": {}
+  },
+  {
+    "description": "very big row",
+    "property": "property",
+    "input": {
+      "count": 1000
+    },
+    "expected": {}
+  }
+]
diff --git a/exercises/practice/pascals-triangle/.meta/tests.toml b/exercises/practice/pascals-triangle/.meta/tests.toml
new file mode 100644
index 0000000..2db0ee5
--- /dev/null
+++ b/exercises/practice/pascals-triangle/.meta/tests.toml
@@ -0,0 +1,34 @@
+# 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.
+
+[9920ce55-9629-46d5-85d6-4201f4a4234d]
+description = "zero rows"
+
+[70d643ce-a46d-4e93-af58-12d88dd01f21]
+description = "single row"
+
+[a6e5a2a2-fc9a-4b47-9f4f-ed9ad9fbe4bd]
+description = "two rows"
+
+[97206a99-79ba-4b04-b1c5-3c0fa1e16925]
+description = "three rows"
+
+[565a0431-c797-417c-a2c8-2935e01ce306]
+description = "four rows"
+
+[06f9ea50-9f51-4eb2-b9a9-c00975686c27]
+description = "five rows"
+
+[c3912965-ddb4-46a9-848e-3363e6b00b13]
+description = "six rows"
+
+[6cb26c66-7b57-4161-962c-81ec8c99f16b]
+description = "ten rows"
diff --git a/exercises/practice/pascals-triangle/PascalsTriangle.lean b/exercises/practice/pascals-triangle/PascalsTriangle.lean
new file mode 100644
index 0000000..f50b4fa
--- /dev/null
+++ b/exercises/practice/pascals-triangle/PascalsTriangle.lean
@@ -0,0 +1,16 @@
+namespace PascalsTriangle
+
+/-
+  Define here a type `Triangle`.
+  Instances of this type are generated wrapped in a suitable monad, through a `mkTriangle` function.
+
+  There must be syntax defined for a `triangle(n)`, where `triangle` is an instance of `Triangle` and `n` is a `Nat`.
+  This syntax should return the `n-th` row of a Pascal's Triangle as an `Array Nat`, wrapped in a suitable monad.
+
+  Try to make your implementation as efficient as possible.
+  There are tests for larger rows that may time out.
+
+  Refer to the test file for more information.
+-/
+
+end PascalsTriangle
diff --git a/exercises/practice/pascals-triangle/PascalsTriangleTest.lean b/exercises/practice/pascals-triangle/PascalsTriangleTest.lean
new file mode 100644
index 0000000..ebb2215
--- /dev/null
+++ b/exercises/practice/pascals-triangle/PascalsTriangleTest.lean
@@ -0,0 +1,97 @@
+import LeanTest
+import PascalsTriangle
+
+open LeanTest
+
+instance : HAppend AssertionResult AssertionResult AssertionResult where
+    hAppend
+        | .success, .success => .success
+        | .failure msg, _    => .failure msg
+        | _, .failure msg    => .failure msg
+
+def pascalsTriangleTests : TestSuite :=
+  (TestSuite.empty "PascalsTriangle")
+  |>.addTest "zero rows" (do
+      let triangle : PascalsTriangle.Triangle ← PascalsTriangle.mkTriangle
+      let mut result := assertEqual #[] (← triangle(0))
+      return result)
+  |>.addTest "single row" (do
+      let triangle : PascalsTriangle.Triangle ← PascalsTriangle.mkTriangle
+      let mut result := assertEqual #[] (← triangle(0))
+      result := result ++ assertEqual #[1] (← triangle(1))
+      return result)
+  |>.addTest "two rows" (do
+      let triangle : PascalsTriangle.Triangle ← PascalsTriangle.mkTriangle
+      let mut result := assertEqual #[] (← triangle(0))
+      result := result ++ assertEqual #[1] (← triangle(1))
+      result := result ++ assertEqual #[1, 1] (← triangle(2))
+      return result)
+  |>.addTest "three rows" (do
+      let triangle : PascalsTriangle.Triangle ← PascalsTriangle.mkTriangle
+      let mut result := assertEqual #[] (← triangle(0))
+      result := result ++ assertEqual #[1] (← triangle(1))
+      result := result ++ assertEqual #[1, 1] (← triangle(2))
+      result := result ++ assertEqual #[1, 2, 1] (← triangle(3))
+      return result)
+  |>.addTest "four rows" (do
+      let triangle : PascalsTriangle.Triangle ← PascalsTriangle.mkTriangle
+      let mut result := assertEqual #[] (← triangle(0))
+      result := result ++ assertEqual #[1] (← triangle(1))
+      result := result ++ assertEqual #[1, 1] (← triangle(2))
+      result := result ++ assertEqual #[1, 2, 1] (← triangle(3))
+      result := result ++ assertEqual #[1, 3, 3, 1] (← triangle(4))
+      return result)
+  |>.addTest "five rows" (do
+      let triangle : PascalsTriangle.Triangle ← PascalsTriangle.mkTriangle
+      let mut result := assertEqual #[] (← triangle(0))
+      result := result ++ assertEqual #[1] (← triangle(1))
+      result := result ++ assertEqual #[1, 1] (← triangle(2))
+      result := result ++ assertEqual #[1, 2, 1] (← triangle(3))
+      result := result ++ assertEqual #[1, 3, 3, 1] (← triangle(4))
+      result := result ++ assertEqual #[1, 4, 6, 4, 1] (← triangle(5))
+      return result)
+  |>.addTest "six rows" (do
+      let triangle : PascalsTriangle.Triangle ← PascalsTriangle.mkTriangle
+      let mut result := assertEqual #[] (← triangle(0))
+      result := result ++ assertEqual #[1] (← triangle(1))
+      result := result ++ assertEqual #[1, 1] (← triangle(2))
+      result := result ++ assertEqual #[1, 2, 1] (← triangle(3))
+      result := result ++ assertEqual #[1, 3, 3, 1] (← triangle(4))
+      result := result ++ assertEqual #[1, 4, 6, 4, 1] (← triangle(5))
+      result := result ++ assertEqual #[1, 5, 10, 10, 5, 1] (← triangle(6))
+      return result)
+  |>.addTest "ten rows" (do
+      let triangle : PascalsTriangle.Triangle ← PascalsTriangle.mkTriangle
+      let mut result := assertEqual #[] (← triangle(0))
+      result := result ++ assertEqual #[1] (← triangle(1))
+      result := result ++ assertEqual #[1, 1] (← triangle(2))
+      result := result ++ assertEqual #[1, 2, 1] (← triangle(3))
+      result := result ++ assertEqual #[1, 3, 3, 1] (← triangle(4))
+      result := result ++ assertEqual #[1, 4, 6, 4, 1] (← triangle(5))
+      result := result ++ assertEqual #[1, 5, 10, 10, 5, 1] (← triangle(6))
+      result := result ++ assertEqual #[1, 6, 15, 20, 15, 6, 1] (← triangle(7))
+      result := result ++ assertEqual #[1, 7, 21, 35, 35, 21, 7, 1] (← triangle(8))
+      result := result ++ assertEqual #[1, 8, 28, 56, 70, 56, 28, 8, 1] (← triangle(9))
+      result := result ++ assertEqual #[1, 9, 36, 84, 126, 126, 84, 36, 9, 1] (← triangle(10))
+      return result)
+  |>.addTest "big row" (do
+      let triangle : PascalsTriangle.Triangle ← PascalsTriangle.mkTriangle
+      let row ← triangle(100)
+      let prev ← triangle(99)
+      let mut result := (assertEqual 100 row.size) ++ (assertEqual 99 prev.size)
+      result := result ++ (assertEqual 1 row[0]!) ++ (assertEqual 1 row[row.size - 1]!)
+      for i in [1:row.size - 1] do
+        result := result ++ assertEqual row[i]! (prev[i - 1]! + prev[i]!)
+      return result)
+  |>.addTest "very big row" (do
+      let triangle : PascalsTriangle.Triangle ← PascalsTriangle.mkTriangle
+      let row ← triangle(1000)
+      let prev ← triangle(999)
+      let mut result := (assertEqual 1000 row.size) ++ (assertEqual 999 prev.size)
+      result := result ++ (assertEqual 1 row[0]!) ++ (assertEqual 1 row[row.size - 1]!)
+      for i in [1:row.size - 1] do
+        result := result ++ assertEqual row[i]! (prev[i - 1]! + prev[i]!)
+      return result)
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [pascalsTriangleTests]
diff --git a/exercises/practice/pascals-triangle/lakefile.toml b/exercises/practice/pascals-triangle/lakefile.toml
new file mode 100644
index 0000000..60a425a
--- /dev/null
+++ b/exercises/practice/pascals-triangle/lakefile.toml
@@ -0,0 +1,15 @@
+name = "pascals-triangle"
+version = "0.1.0"
+defaultTargets = ["PascalsTriangleTest"]
+testDriver = "PascalsTriangleTest"
+
+[[lean_lib]]
+name = "LeanTest"
+srcDir = "vendor/LeanTest"
+
+[[lean_lib]]
+name = "PascalsTriangle"
+
+[[lean_exe]]
+name = "PascalsTriangleTest"
+root = "PascalsTriangleTest"
diff --git a/exercises/practice/pascals-triangle/lean-toolchain b/exercises/practice/pascals-triangle/lean-toolchain
new file mode 100644
index 0000000..14791d7
--- /dev/null
+++ b/exercises/practice/pascals-triangle/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.29.0
diff --git a/exercises/practice/pascals-triangle/vendor/LeanTest/LeanTest.lean b/exercises/practice/pascals-triangle/vendor/LeanTest/LeanTest.lean
new file mode 100644
index 0000000..012ba20
--- /dev/null
+++ b/exercises/practice/pascals-triangle/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/pascals-triangle/vendor/LeanTest/LeanTest/Assertions.lean b/exercises/practice/pascals-triangle/vendor/LeanTest/LeanTest/Assertions.lean
new file mode 100644
index 0000000..60e4ad8
--- /dev/null
+++ b/exercises/practice/pascals-triangle/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/pascals-triangle/vendor/LeanTest/LeanTest/Test.lean b/exercises/practice/pascals-triangle/vendor/LeanTest/LeanTest/Test.lean
new file mode 100644
index 0000000..5ddbae5
--- /dev/null
+++ b/exercises/practice/pascals-triangle/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 969f480..527d9d4 100644
--- a/generators/Generator/Generator.lean
+++ b/generators/Generator/Generator.lean
@@ -1,3 +1,4 @@
+import Generator.PascalsTriangleGenerator
 import Generator.ResistorColorDuoGenerator
 import Generator.VariableLengthQuantityGenerator
 import Generator.ReverseListGenerator
@@ -105,6 +106,7 @@ abbrev endBodyGenerator := String -> String
 
 def dispatch : Std.HashMap String (introGenerator × testCaseGenerator × endBodyGenerator) :=
   Std.HashMap.ofList [
+    ("PascalsTriangle", (PascalsTriangleGenerator.genIntro, PascalsTriangleGenerator.genTestCase, PascalsTriangleGenerator.genEnd)),
     ("ResistorColorDuo", (ResistorColorDuoGenerator.genIntro, ResistorColorDuoGenerator.genTestCase, ResistorColorDuoGenerator.genEnd)),
     ("VariableLengthQuantity", (VariableLengthQuantityGenerator.genIntro, VariableLengthQuantityGenerator.genTestCase, VariableLengthQuantityGenerator.genEnd)),
     ("ReverseList", (ReverseListGenerator.genIntro, ReverseListGenerator.genTestCase, ReverseListGenerator.genEnd)),
diff --git a/generators/Generator/Generator/PascalsTriangleGenerator.lean b/generators/Generator/Generator/PascalsTriangleGenerator.lean
new file mode 100644
index 0000000..9f2f03e
--- /dev/null
+++ b/generators/Generator/Generator/PascalsTriangleGenerator.lean
@@ -0,0 +1,61 @@
+import Lean.Data.Json
+import Std
+import Helper
+
+open Lean
+open Std
+open Helper
+
+namespace PascalsTriangleGenerator
+
+def genIntro (exercise : String) : String := s!"import LeanTest
+import {exercise}
+
+open LeanTest
+
+{concatAsserts}
+
+def {exercise.decapitalize}Tests : TestSuite :=
+  (TestSuite.empty \"{exercise}\")"
+
+def genTestCase (exercise : String) (case : TreeMap.Raw String Json) : String :=
+  let count := case.get! "input" |>.getObjValD "count" |>.getNat? |> getOk
+  let expected := case.get! "expected" |>.getArr? |> getOk
+  let description := case.get! "description"
+              |> (·.compress)
+  let funName := getFunName (case.get! "property")
+  let call := s!"{exercise}.mkTriangle"
+  match funName with
+  | "rows" =>
+    s!"
+  |>.addTest {description} (do
+      let triangle : {exercise}.Triangle ← {call}
+      {(Id.run do
+        let start := s!"let mut result := assertEqual #[] (← triangle(0))"
+        let mut res := [start]
+        for n in [:expected.size] do
+          let row := expected[n]!
+          res := s!"      result := result ++ assertEqual #{row} (← triangle({n + 1}))" :: res
+        return String.intercalate "\n" res.reverse)}
+      return result)"
+  | "property" =>
+    s!"
+  |>.addTest {description} (do
+      let triangle : {exercise}.Triangle ← {call}
+      let row ← triangle({count})
+      let prev ← triangle({count - 1})
+      let mut result := (assertEqual {count} row.size) ++ (assertEqual {count - 1} prev.size)
+      result := result ++ (assertEqual 1 row[0]!) ++ (assertEqual 1 row[row.size - 1]!)
+      for i in [1:row.size - 1] do
+        result := result ++ assertEqual row[i]! (prev[i - 1]! + prev[i]!)
+      return result)"
+  | _ => ""
+
+def genEnd (exercise : String) : String :=
+  s!"
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [{exercise.decapitalize}Tests]
+"
+
+end PascalsTriangleGenerator