diff --git a/config.json b/config.json
index fdca7a1..282da51 100644
--- a/config.json
+++ b/config.json
@@ -425,6 +425,14 @@
         "prerequisites": [],
         "difficulty": 6
       },
+      {
+        "slug": "camicia",
+        "name": "Camicia",
+        "uuid": "38e10910-8c63-4925-a8db-2fd182b5ccc4",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 6
+      },
       {
         "slug": "complex-numbers",
         "name": "Complex Numbers",
diff --git a/exercises/practice/camicia/.docs/instructions.md b/exercises/practice/camicia/.docs/instructions.md
new file mode 100644
index 0000000..db62fce
--- /dev/null
+++ b/exercises/practice/camicia/.docs/instructions.md
@@ -0,0 +1,84 @@
+# Instructions
+
+In this exercise, you will simulate a game very similar to the classic card game **Camicia**.
+Your program will receive the initial configuration of two players' decks and must simulate the game until it ends (or detect that it will never end).
+
+## Rules
+
+- The deck is split between **two players**.
+  The player's cards are read from left to right, where the leftmost card is the top of the deck.
+- A round consists of both players playing at least one card.
+- Players take turns placing the **top card** of their deck onto a central pile.
+- If the card is a **number card** (2-10), play simply passes to the other player.
+- If the card is a **payment card**, a penalty must be paid:
+  - **J** → opponent must pay 1 card
+  - **Q** → opponent must pay 2 cards
+  - **K** → opponent must pay 3 cards
+  - **A** → opponent must pay 4 cards
+- If the player paying a penalty reveals another payment card, that player stops paying the penalty.
+  The other player must then pay a penalty based on the new payment card.
+- If the penalty is fully paid without interruption, the player who placed the **last payment card** collects the central pile and places it at the bottom of their deck.
+  That player then starts the next round.
+- If a player runs out of cards and is unable to play a card (either while paying a penalty or when it is their turn), the other player collects the central pile.
+- The moment when a player collects cards from the central pile is called a **trick**.
+- If a player has all the cards in their possession after a trick, the game **ends**.
+- The game **enters a loop** as soon as the decks are identical to what they were earlier during the game, **not** counting number cards!
+
+## Examples
+
+A small example of a match that ends.
+
+| Round | Player A     | Player B                   | Pile                       | Penalty Due |
+| :---- | :----------- | :------------------------- | :------------------------- | :---------- |
+| 1     | 2 A 7 8 Q 10 | 3 4 5 6 K 9 J              |                            | -           |
+| 1     | A 7 8 Q 10   | 3 4 5 6 K 9 J              | 2                          | -           |
+| 1     | A 7 8 Q 10   | 4 5 6 K 9 J                | 2 3                        | -           |
+| 1     | 7 8 Q 10     | 4 5 6 K 9 J                | 2 3 A                      | Player B: 4 |
+| 1     | 7 8 Q 10     | 5 6 K 9 J                  | 2 3 A 4                    | Player B: 3 |
+| 1     | 7 8 Q 10     | 6 K 9 J                    | 2 3 A 4 5                  | Player B: 2 |
+| 1     | 7 8 Q 10     | K 9 J                      | 2 3 A 4 5 6                | Player B: 1 |
+| 1     | 7 8 Q 10     | 9 J                        | 2 3 A 4 5 6 K              | Player A: 3 |
+| 1     | 8 Q 10       | 9 J                        | 2 3 A 4 5 6 K 7            | Player A: 2 |
+| 1     | Q 10         | 9 J                        | 2 3 A 4 5 6 K 7 8          | Player A: 1 |
+| 1     | 10           | 9 J                        | 2 3 A 4 5 6 K 7 8 Q        | Player B: 2 |
+| 1     | 10           | J                          | 2 3 A 4 5 6 K 7 8 Q 9      | Player B: 1 |
+| 1     | 10           | -                          | 2 3 A 4 5 6 K 7 8 Q 9 J    | Player A: 1 |
+| 1     | -            | -                          | 2 3 A 4 5 6 K 7 8 Q 9 J 10 | -           |
+| 2     | -            | 2 3 A 4 5 6 K 7 8 Q 9 J 10 | -                          | -           |
+
+status: `"finished"`, cards: 13, tricks: 1
+
+This is a small example of a match that loops.
+
+| Round | Player A | Player B | Pile  | Penalty Due |
+| :---- | :------- | :------- | :---- | :---------- |
+| 1     | J 2 3    | 4 J 5    | -     | -           |
+| 1     | 2 3      | 4 J 5    | J     | Player B: 1 |
+| 1     | 2 3      | J 5      | J 4   | -           |
+| 2     | 2 3 J 4  | J 5      | -     | -           |
+| 2     | 3 J 4    | J 5      | 2     | -           |
+| 2     | 3 J 4    | 5        | 2 J   | Player A: 1 |
+| 2     | J 4      | 5        | 2 J 3 | -           |
+| 3     | J 4      | 5 2 J 3  | -     | -           |
+| 3     | J 4      | 2 J 3    | 5     | -           |
+| 3     | 4        | 2 J 3    | 5 J   | Player B: 1 |
+| 3     | 4        | J 3      | 5 J 2 | -           |
+| 4     | 4 5 J 2  | J 3      | -     | -           |
+
+The start of round 4 matches the start of round 2.
+Recall, the value of the number cards does not matter.
+
+status: `"loop"`, cards: 8, tricks: 3
+
+## Your Task
+
+- Using the input, simulate the game following the rules above.
+- Determine the following information regarding the game:
+  - **Status**: `"finished"` or `"loop"`
+  - **Cards**: total number of cards played throughout the game
+  - **Tricks**: number of times the central pile was collected
+
+~~~~exercism/advanced
+For those who want to take on a more exciting challenge, the hunt for other records for the longest game with an end is still open.
+There are 653,534,134,886,878,245,000 (approximately 654 quintillion) possibilities, and we haven't calculated them all yet!
+~~~~
diff --git a/exercises/practice/camicia/.docs/introduction.md b/exercises/practice/camicia/.docs/introduction.md
new file mode 100644
index 0000000..761d8a8
--- /dev/null
+++ b/exercises/practice/camicia/.docs/introduction.md
@@ -0,0 +1,24 @@
+# Introduction
+
+One rainy afternoon, you sit at the kitchen table playing cards with your grandmother.
+The game is her take on [Camicia][bmn].
+
+At first it feels like just another friendly match: cards slapped down, laughter across the table, the occasional victorious grin from Nonna.
+But as the game stretches on, something strange happens.
+The same cards keep cycling back.
+You play card after card, yet the end never seems to come.
+
+You start to wonder.
+_Will this game ever finish?
+Or could we keep playing forever?_
+
+Later, driven by curiosity, you search online and to your surprise you discover that what happened wasn't just bad luck.
+You and your grandmother may have stumbled upon one of the longest possible sequences!
+Suddenly, you're hooked.
+What began as a casual game has turned into a quest: _how long can such a game really last?_
+_Can you find a sequence even longer than the one you played at the kitchen table?_
+_Perhaps even long enough to set a new world record?_
+
+And so, armed with nothing but a deck of cards and some algorithmic ingenuity, you decide to investigate...
+
+[bmn]: https://en.wikipedia.org/wiki/Beggar-my-neighbour
diff --git a/exercises/practice/camicia/.meta/Example.lean b/exercises/practice/camicia/.meta/Example.lean
new file mode 100644
index 0000000..68995a6
--- /dev/null
+++ b/exercises/practice/camicia/.meta/Example.lean
@@ -0,0 +1,64 @@
+import Std
+
+namespace Camicia
+
+inductive Card where
+  | C2 | C3 | C4 | C5 | C6 | C7 | C8 | C9
+  | C10 | CJ | CQ | CK | CA
+  deriving BEq, Repr, Nonempty
+
+inductive Status where
+  | finished | loop
+  deriving BEq, Repr, Nonempty
+
+structure Result where
+  status : Status
+  cards  : Nat
+  tricks : Nat
+  deriving BEq, Repr, Nonempty
+
+inductive Turn where
+  | playerA | playerB
+  deriving BEq, Repr, Nonempty
+
+def Card.value : Card -> Nat
+  | .C2 | .C3 | .C4 | .C5 | .C6 | .C7 | .C8 | .C9 | .C10 => 0
+  | .CJ => 1
+  | .CQ => 2
+  | .CK => 3
+  | .CA => 4
+
+abbrev NumCards := Nat
+abbrev NumTricks := Nat
+abbrev Penalty := Nat
+abbrev Deck := List Nat
+abbrev Pile := List Nat
+
+partial def takeTurn : Turn -> Deck -> Deck -> Pile -> NumCards -> NumTricks -> Penalty -> Std.HashSet (Deck × Deck) -> Result
+  | .playerA, [], _, _, cards, tricks, _, _
+  | .playerB, _, [], _, cards, tricks, _, _                         => { status := .finished, cards := cards, tricks := tricks + 1 }
+  | .playerA, 0 :: deckA, deckB, pile, cards, tricks, 0, seen       => takeTurn .playerB deckA deckB (0 :: pile) (cards + 1) tricks 0 seen
+  | .playerB, deckA, 0 :: deckB, pile, cards, tricks, 0, seen       => takeTurn .playerA deckA deckB (0 :: pile) (cards + 1) tricks 0 seen
+  | .playerA, [0], _, _, cards, tricks, 1, _
+  | .playerB, _, [0], _, cards, tricks, 1, _                        => { status := .finished, cards := cards + 1, tricks := tricks + 1 }
+  | .playerA, 0 :: deckA, deckB, pile, cards, tricks, 1, seen       =>
+      let newDeckB := deckB ++ (0 :: pile).reverse
+      if seen.contains (deckA, newDeckB)
+      then { status := .loop, cards := cards + 1, tricks := tricks + 1 }
+      else takeTurn .playerB deckA newDeckB [] (cards + 1) (tricks + 1) 0 (seen.insert (deckA, newDeckB))
+  | .playerB, deckA, 0 :: deckB, pile, cards, tricks, 1, seen       =>
+      let newDeckA := deckA ++ (0 :: pile).reverse
+      if seen.contains (newDeckA, deckB)
+      then { status := .loop, cards := cards + 1, tricks := tricks + 1 }
+      else takeTurn .playerA newDeckA deckB [] (cards + 1) (tricks + 1) 0 (seen.insert (newDeckA, deckB))
+  | .playerA, 0 :: deckA, deckB, pile, cards, tricks, penalty, seen => takeTurn .playerA deckA deckB (0 :: pile) (cards + 1) tricks (penalty - 1) seen
+  | .playerB, deckA, 0 :: deckB, pile, cards, tricks, penalty, seen => takeTurn .playerB deckA deckB (0 :: pile) (cards + 1) tricks (penalty - 1) seen
+  | .playerA, n :: deckA, deckB, pile, cards, tricks, _, seen       => takeTurn .playerB deckA deckB (n :: pile) (cards + 1) tricks n seen
+  | .playerB, deckA, n :: deckB, pile, cards, tricks, _, seen       => takeTurn .playerA deckA deckB (n :: pile) (cards + 1) tricks n seen
+
+def simulateGame (playerA playerB : List Card) : Result :=
+  let deckA := playerA.map Card.value
+  let deckB := playerB.map Card.value
+  takeTurn .playerA deckA deckB [] 0 0 0 (.ofList [(deckA, deckB)])
+
+end Camicia
diff --git a/exercises/practice/camicia/.meta/config.json b/exercises/practice/camicia/.meta/config.json
new file mode 100644
index 0000000..96fa60b
--- /dev/null
+++ b/exercises/practice/camicia/.meta/config.json
@@ -0,0 +1,19 @@
+{
+  "authors": [
+    "oxe-i"
+  ],
+  "files": {
+    "solution": [
+      "Camicia.lean"
+    ],
+    "test": [
+      "CamiciaTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Simulate the card game and determine whether the match ends or enters an infinite loop.",
+  "source": "Beggar-My-Neighbour",
+  "source_url": "https://www.richardpmann.com/beggar-my-neighbour-records.html"
+}
diff --git a/exercises/practice/camicia/.meta/tests.toml b/exercises/practice/camicia/.meta/tests.toml
new file mode 100644
index 0000000..18d3fdd
--- /dev/null
+++ b/exercises/practice/camicia/.meta/tests.toml
@@ -0,0 +1,94 @@
+# 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.
+
+[0b7f737c-3ecd-4a55-b34d-e65c62a85c28]
+description = "two cards, one trick"
+
+[27c19d75-53a5-48e5-b33b-232c3884d4f3]
+description = "three cards, one trick"
+
+[9b02dd49-efaf-4b71-adca-a05c18a7c5b0]
+description = "four cards, one trick"
+
+[fa3f4479-466a-4734-a001-ab79bfe27260]
+description = "the ace reigns supreme"
+
+[07629689-f589-4f54-a6d1-8ce22776ce72]
+description = "the king beats ace"
+
+[54d4a1c5-76fb-4d1e-8358-0e0296ac0601]
+description = "the queen seduces the king"
+
+[c875500c-ff3d-47a4-bd1e-b60b90da80aa]
+description = "the jack betrays the queen"
+
+[436875da-96ca-4149-be22-0b78173b8125]
+description = "the 10 just wants to put on a show"
+
+[5be39bb6-1b34-4ce6-a1cd-0fcc142bb272]
+description = "simple loop with decks of 3 cards"
+
+[2795dc21-0a2a-4c38-87c2-5a42e1ff15eb]
+description = "the story is starting to get a bit complicated"
+
+[6999dfac-3fdc-41e2-b64b-38f4be228712]
+description = "two tricks"
+
+[83dcd4f3-e089-4d54-855a-73f5346543a3]
+description = "more tricks"
+
+[3107985a-f43e-486a-9ce8-db51547a9941]
+description = "simple loop with decks of 4 cards"
+
+[dca32c31-11ed-49f6-b078-79ab912c1f7b]
+description = "easy card combination"
+
+[1f8488d0-48d3-45ae-b819-59cedad0a5f4]
+description = "easy card combination, inverted decks"
+
+[98878d35-623a-4d05-b81a-7bdc569eb88d]
+description = "mirrored decks"
+
+[3e0ba597-ca10-484b-87a3-31a7df7d6da3]
+description = "opposite decks"
+
+[92334ddb-aaa7-47fa-ab36-e928a8a6a67c]
+description = "random decks #1"
+
+[30477523-9651-4860-84a3-e1ac461bb7fa]
+description = "random decks #2"
+
+[20967de8-9e94-4e0e-9010-14bc1c157432]
+description = "Kleber 1999"
+
+[9f2fdfe8-27f3-4323-816d-6bce98a9c6f7]
+description = "Collins 2006"
+
+[c90b6f8d-7013-49f3-b5cb-14ea006cca1d]
+description = "Mann and Wu 2007"
+
+[a3f1fbc5-1d0b-499a-92a5-22932dfc6bc8]
+description = "Nessler 2012"
+
+[9cefb1ba-e6d1-4ab7-9d8f-76d8e0976d5f]
+description = "Anderson 2013"
+
+[d37c0318-5be6-48d0-ab72-a7aaaff86179]
+description = "Rucklidge 2014"
+
+[4305e479-ba87-432f-8a29-cd2bd75d2f05]
+description = "Nessler 2021"
+
+[252f5cc3-b86d-4251-87ce-f920b7a6a559]
+description = "Nessler 2022"
+
+[b9efcfa4-842f-4542-8112-8389c714d958]
+description = "Casella 2024, first infinite game found"
diff --git a/exercises/practice/camicia/Camicia.lean b/exercises/practice/camicia/Camicia.lean
new file mode 100644
index 0000000..85af0ba
--- /dev/null
+++ b/exercises/practice/camicia/Camicia.lean
@@ -0,0 +1,21 @@
+namespace Camicia
+
+inductive Card where
+  | C2 | C3 | C4 | C5 | C6 | C7 | C8 | C9
+  | C10 | CJ | CQ | CK | CA
+  deriving BEq, Repr
+
+inductive Status where
+  | finished | loop
+  deriving BEq, Repr
+
+structure Result where
+  status : Status
+  cards  : Nat
+  tricks : Nat
+  deriving BEq, Repr
+
+def simulateGame (playerA playerB : List Card) : Result :=
+  sorry
+
+end Camicia
diff --git a/exercises/practice/camicia/CamiciaTest.lean b/exercises/practice/camicia/CamiciaTest.lean
new file mode 100644
index 0000000..0b9660d
--- /dev/null
+++ b/exercises/practice/camicia/CamiciaTest.lean
@@ -0,0 +1,66 @@
+import LeanTest
+import Camicia
+
+open LeanTest
+
+def camiciaTests : TestSuite :=
+  (TestSuite.empty "Camicia")
+  |>.addTest "two cards, one trick" (do
+      return assertEqual ⟨.finished, 2, 1⟩ (Camicia.simulateGame [.C2] [.C3]))
+  |>.addTest "three cards, one trick" (do
+      return assertEqual ⟨.finished, 3, 1⟩ (Camicia.simulateGame [.C2, .C4] [.C3]))
+  |>.addTest "four cards, one trick" (do
+      return assertEqual ⟨.finished, 4, 1⟩ (Camicia.simulateGame [.C2, .C4] [.C3, .C5, .C6]))
+  |>.addTest "the ace reigns supreme" (do
+      return assertEqual ⟨.finished, 7, 1⟩ (Camicia.simulateGame [.C2, .CA] [.C3, .C4, .C5, .C6, .C7]))
+  |>.addTest "the king beats ace" (do
+      return assertEqual ⟨.finished, 7, 1⟩ (Camicia.simulateGame [.C2, .CA] [.C3, .C4, .C5, .C6, .CK]))
+  |>.addTest "the queen seduces the king" (do
+      return assertEqual ⟨.finished, 10, 1⟩ (Camicia.simulateGame [.C2, .CA, .C7, .C8, .CQ] [.C3, .C4, .C5, .C6, .CK]))
+  |>.addTest "the jack betrays the queen" (do
+      return assertEqual ⟨.finished, 12, 1⟩ (Camicia.simulateGame [.C2, .CA, .C7, .C8, .CQ] [.C3, .C4, .C5, .C6, .CK, .C9, .CJ]))
+  |>.addTest "the 10 just wants to put on a show" (do
+      return assertEqual ⟨.finished, 13, 1⟩ (Camicia.simulateGame [.C2, .CA, .C7, .C8, .CQ, .C10] [.C3, .C4, .C5, .C6, .CK, .C9, .CJ]))
+  |>.addTest "simple loop with decks of 3 cards" (do
+      return assertEqual ⟨.loop, 8, 3⟩ (Camicia.simulateGame [.CJ, .C2, .C3] [.C4, .CJ, .C5]))
+  |>.addTest "the story is starting to get a bit complicated" (do
+      return assertEqual ⟨.finished, 361, 1⟩ (Camicia.simulateGame [.C2, .C6, .C6, .CJ, .C4, .CK, .CQ, .C10, .CK, .CJ, .CQ, .C2, .C3, .CK, .C5, .C6, .CQ, .CQ, .CA, .CA, .C6, .C9, .CK, .CA, .C8, .CK, .C2, .CA, .C9, .CA, .CQ, .C4, .CK, .CK, .CK, .C3, .C5, .CK, .C8, .CQ, .C3, .CQ, .C7, .CJ, .CK, .CJ, .C9, .CJ, .C3, .C3, .CK, .CK, .CQ, .CA, .CK, .C7, .C10, .CA, .CQ, .C7, .C10, .CJ, .C4, .C5, .CJ, .C9, .C10, .CQ, .CJ, .CJ, .CK, .C6, .C10, .CJ, .C6, .CQ, .CJ, .C5, .CJ, .CQ, .CQ, .C8, .C3, .C8, .CA, .C2, .C6, .C9, .CK, .C7, .CJ, .CK, .CK, .C8, .CK, .CQ, .C6, .C10, .CJ, .C10, .CJ, .CQ, .CJ, .C10, .C3, .C8, .CK, .CA, .C6, .C9, .CK, .C2, .CA, .CA, .C10, .CJ, .C6, .CA, .C4, .CJ, .CA, .CJ, .CJ, .C6, .C2, .CJ, .C3, .CK, .C2, .C5, .C9, .CJ, .C9, .C6, .CK, .CA, .C5, .CQ, .CJ, .C2, .CQ, .CK, .CA, .C3, .CK, .CJ, .CK, .C2, .C5, .C6, .CQ, .CJ, .CQ, .CQ, .CJ, .C2, .CJ, .C9, .CQ, .C7, .C7, .CA, .CQ, .C7, .CQ, .CJ, .CK, .CJ, .CA, .C7, .C7, .C8, .CQ, .C10, .CJ, .C10, .CJ, .CJ, .C9, .C2, .CA, .C2] [.C7, .C2, .C10, .CK, .C8, .C2, .CJ, .C9, .CA, .C5, .C6, .CJ, .CQ, .C6, .CK, .C6, .C5, .CA, .C4, .CQ, .C7, .CJ, .C7, .C10, .C2, .CQ, .C8, .C2, .C2, .CK, .CJ, .CA, .C5, .C5, .CA, .C4, .CQ, .C6, .CQ, .CK, .C10, .C8, .CQ, .C2, .C10, .CJ, .CA, .CQ, .C8, .CQ, .CQ, .CJ, .CJ, .CA, .CA, .C9, .C10, .CJ, .CK, .C4, .CQ, .C10, .C10, .CJ, .CK, .C10, .C2, .CJ, .C7, .CA, .CK, .CK, .CJ, .CA, .CJ, .C10, .C8, .CK, .CA, .C7, .CQ, .CQ, .CJ, .C3, .CQ, .C4, .CA, .C3, .CA, .CQ, .CQ, .CQ, .C5, .C4, .CK, .CJ, .C10, .CA, .CQ, .CJ, .C6, .CJ, .CA, .C10, .CA, .C5, .C8, .C3, .CK, .C5, .C9, .CQ, .C8, .C7, .C7, .CJ, .C7, .CQ, .CQ, .CQ, .CA, .C7, .C8, .C9, .CA, .CQ, .CA, .CK, .C8, .CA, .CA, .CJ, .C8, .C4, .C8, .CK, .CJ, .CA, .C10, .CQ, .C8, .CJ, .C8, .C6, .C10, .CQ, .CJ, .CJ, .CA, .CA, .CJ, .C5, .CQ, .C6, .CJ, .CK, .CQ, .C8, .CK, .C4, .CQ, .CQ, .C6, .CJ, .CK, .C4, .C7, .CJ, .CJ, .C9, .C9, .CA, .CQ, .CQ, .CK, .CA, .C6, .C5, .CK]))
+  |>.addTest "two tricks" (do
+      return assertEqual ⟨.finished, 5, 2⟩ (Camicia.simulateGame [.CJ] [.C3, .CJ]))
+  |>.addTest "more tricks" (do
+      return assertEqual ⟨.finished, 12, 4⟩ (Camicia.simulateGame [.CJ, .C2, .C4] [.C3, .CJ, .CA]))
+  |>.addTest "simple loop with decks of 4 cards" (do
+      return assertEqual ⟨.loop, 16, 4⟩ (Camicia.simulateGame [.C2, .C3, .CJ, .C6] [.CK, .C5, .CJ, .C7]))
+  |>.addTest "easy card combination" (do
+      return assertEqual ⟨.finished, 40, 4⟩ (Camicia.simulateGame [.C4, .C8, .C7, .C5, .C4, .C10, .C3, .C9, .C7, .C3, .C10, .C10, .C6, .C8, .C2, .C8, .C5, .C4, .C5, .C9, .C6, .C5, .C2, .C8, .C10, .C9] [.C6, .C9, .C4, .C7, .C2, .C2, .C3, .C6, .C7, .C3, .CA, .CA, .CA, .CA, .CK, .CK, .CK, .CK, .CQ, .CQ, .CQ, .CQ, .CJ, .CJ, .CJ, .CJ]))
+  |>.addTest "easy card combination, inverted decks" (do
+      return assertEqual ⟨.finished, 40, 4⟩ (Camicia.simulateGame [.C3, .C3, .C5, .C7, .C3, .C2, .C10, .C7, .C6, .C7, .CA, .CA, .CA, .CA, .CK, .CK, .CK, .CK, .CQ, .CQ, .CQ, .CQ, .CJ, .CJ, .CJ, .CJ] [.C5, .C10, .C8, .C2, .C6, .C7, .C2, .C4, .C9, .C2, .C6, .C10, .C10, .C5, .C4, .C8, .C4, .C8, .C6, .C9, .C8, .C5, .C9, .C3, .C4, .C9]))
+  |>.addTest "mirrored decks" (do
+      return assertEqual ⟨.finished, 59, 4⟩ (Camicia.simulateGame [.C2, .CA, .C3, .CA, .C3, .CK, .C4, .CK, .C2, .CQ, .C2, .CQ, .C10, .CJ, .C5, .CJ, .C6, .C10, .C2, .C9, .C10, .C7, .C3, .C9, .C6, .C9] [.C6, .CA, .C4, .CA, .C7, .CK, .C4, .CK, .C7, .CQ, .C7, .CQ, .C5, .CJ, .C8, .CJ, .C4, .C5, .C8, .C9, .C10, .C6, .C8, .C3, .C8, .C5]))
+  |>.addTest "opposite decks" (do
+      return assertEqual ⟨.finished, 151, 21⟩ (Camicia.simulateGame [.C4, .CA, .C9, .CA, .C4, .CK, .C9, .CK, .C6, .CQ, .C8, .CQ, .C8, .CJ, .C10, .CJ, .C9, .C8, .C4, .C6, .C3, .C6, .C5, .C2, .C4, .C3] [.C10, .C7, .C3, .C2, .C9, .C2, .C7, .C8, .C7, .C5, .CJ, .C7, .CJ, .C10, .CQ, .C10, .CQ, .C3, .CK, .C5, .CK, .C6, .CA, .C2, .CA, .C5]))
+  |>.addTest "random decks #1" (do
+      return assertEqual ⟨.finished, 542, 76⟩ (Camicia.simulateGame [.CK, .C10, .C9, .C8, .CJ, .C8, .C6, .C9, .C7, .CA, .CK, .C5, .C4, .C4, .CJ, .C5, .CJ, .C4, .C3, .C5, .C8, .C6, .C7, .C7, .C4, .C9] [.C6, .C3, .CK, .CA, .CQ, .C10, .CA, .C2, .CQ, .C8, .C2, .C10, .C10, .C2, .CQ, .C3, .CK, .C9, .C7, .CA, .C3, .CQ, .C5, .CJ, .C2, .C6]))
+  |>.addTest "random decks #2" (do
+      return assertEqual ⟨.finished, 327, 42⟩ (Camicia.simulateGame [.C8, .CA, .C4, .C8, .C5, .CQ, .CJ, .C2, .C6, .C2, .C9, .C7, .CK, .CA, .C8, .C10, .CK, .C8, .C10, .C9, .CK, .C6, .C7, .C3, .CK, .C9] [.C10, .C5, .C2, .C6, .CQ, .CJ, .CA, .C9, .C5, .C5, .C3, .C7, .C3, .CJ, .CA, .C2, .CQ, .C3, .CJ, .CQ, .C4, .C10, .C4, .C7, .C4, .C6]))
+  |>.addTest "Kleber 1999" (do
+      return assertEqual ⟨.finished, 5790, 805⟩ (Camicia.simulateGame [.C4, .C8, .C9, .CJ, .CQ, .C8, .C5, .C5, .CK, .C2, .CA, .C9, .C8, .C5, .C10, .CA, .C4, .CJ, .C3, .CK, .C6, .C9, .C2, .CQ, .CK, .C7] [.C10, .CJ, .C3, .C2, .C4, .C10, .C4, .C7, .C5, .C3, .C6, .C6, .C7, .CA, .CJ, .CQ, .CA, .C7, .C2, .C10, .C3, .CK, .C9, .C6, .C8, .CQ]))
+  |>.addTest "Collins 2006" (do
+      return assertEqual ⟨.finished, 6913, 960⟩ (Camicia.simulateGame [.CA, .C8, .CQ, .CK, .C9, .C10, .C3, .C7, .C4, .C2, .CQ, .C3, .C2, .C10, .C9, .CK, .CA, .C8, .C7, .C7, .C4, .C5, .CJ, .C9, .C2, .C10] [.C4, .CJ, .CA, .CK, .C8, .C5, .C6, .C6, .CA, .C6, .C5, .CQ, .C4, .C6, .C10, .C8, .CJ, .C2, .C5, .C7, .CQ, .CJ, .C3, .C3, .CK, .C9]))
+  |>.addTest "Mann and Wu 2007" (do
+      return assertEqual ⟨.finished, 7157, 1007⟩ (Camicia.simulateGame [.CK, .C2, .CK, .CK, .C3, .C3, .C6, .C10, .CK, .C6, .CA, .C2, .C5, .C5, .C7, .C9, .CJ, .CA, .CA, .C3, .C4, .CQ, .C4, .C8, .CJ, .C6] [.C4, .C5, .C2, .CQ, .C7, .C9, .C9, .CQ, .C7, .CJ, .C9, .C8, .C10, .C3, .C10, .CJ, .C4, .C10, .C8, .C6, .C8, .C7, .CA, .CQ, .C5, .C2]))
+  |>.addTest "Nessler 2012" (do
+      return assertEqual ⟨.finished, 7207, 1015⟩ (Camicia.simulateGame [.C10, .C3, .C6, .C7, .CQ, .C2, .C9, .C8, .C2, .C8, .C4, .CA, .C10, .C6, .CK, .C2, .C10, .CA, .C5, .CA, .C2, .C4, .CQ, .CJ, .CK, .C4] [.C10, .CQ, .C4, .C6, .CJ, .C9, .C3, .CJ, .C9, .C3, .C3, .CQ, .CK, .C5, .C9, .C5, .CK, .C6, .C5, .C7, .C8, .CJ, .CA, .C7, .C8, .C7]))
+  |>.addTest "Anderson 2013" (do
+      return assertEqual ⟨.finished, 7225, 1016⟩ (Camicia.simulateGame [.C6, .C7, .CA, .C3, .CQ, .C3, .C5, .CJ, .C3, .C2, .CJ, .C7, .C4, .C5, .CQ, .C10, .C5, .CA, .CJ, .C2, .CK, .C8, .C9, .C9, .CK, .C3] [.C4, .CJ, .C6, .C9, .C8, .C5, .C10, .C7, .C9, .CQ, .C2, .C7, .C10, .C8, .C4, .C10, .CA, .C6, .C4, .CA, .C6, .C8, .CQ, .CK, .CK, .C2]))
+  |>.addTest "Rucklidge 2014" (do
+      return assertEqual ⟨.finished, 7959, 1122⟩ (Camicia.simulateGame [.C8, .CJ, .C2, .C9, .C4, .C4, .C5, .C8, .CQ, .C3, .C9, .C3, .C6, .C2, .C8, .CA, .CA, .CA, .C9, .C4, .C7, .C2, .C5, .CQ, .CQ, .C3] [.CK, .C7, .C10, .C6, .C3, .CJ, .CA, .C7, .C6, .C5, .C5, .C8, .C10, .C9, .C10, .C4, .C2, .C7, .CK, .CQ, .C10, .CK, .C6, .CJ, .CJ, .CK]))
+  |>.addTest "Nessler 2021" (do
+      return assertEqual ⟨.finished, 7972, 1106⟩ (Camicia.simulateGame [.C7, .C2, .C3, .C4, .CK, .C9, .C6, .C10, .CA, .C8, .C9, .CQ, .C7, .CA, .C4, .C8, .CJ, .CJ, .CA, .C4, .C3, .C2, .C5, .C6, .C6, .CJ] [.C3, .C10, .C8, .C9, .C8, .CK, .CK, .C2, .C5, .C5, .C7, .C6, .C4, .C3, .C5, .C7, .CA, .C9, .CJ, .CK, .C2, .CQ, .C10, .CQ, .C10, .CQ]))
+  |>.addTest "Nessler 2022" (do
+      return assertEqual ⟨.finished, 8344, 1164⟩ (Camicia.simulateGame [.C2, .C10, .C10, .CA, .CJ, .C3, .C8, .CQ, .C2, .C5, .C5, .C5, .C9, .C2, .C4, .C3, .C10, .CQ, .CA, .CK, .CQ, .CJ, .CJ, .C9, .CQ, .CK] [.C10, .C7, .C6, .C3, .C6, .CA, .C8, .C9, .C4, .C3, .CK, .CJ, .C6, .CK, .C4, .C9, .C7, .C8, .C5, .C7, .C8, .C2, .CA, .C7, .C4, .C6]))
+  |>.addTest "Casella 2024, first infinite game found" (do
+      return assertEqual ⟨.loop, 474, 66⟩ (Camicia.simulateGame [.C2, .C8, .C4, .CK, .C5, .C2, .C3, .CQ, .C6, .CK, .CQ, .CA, .CJ, .C3, .C5, .C9, .C8, .C3, .CA, .CA, .CJ, .C4, .C4, .CJ, .C7, .C5] [.C7, .C7, .C8, .C6, .C10, .C10, .C6, .C10, .C7, .C2, .CQ, .C6, .C3, .C2, .C4, .CK, .CQ, .C10, .CJ, .C5, .C9, .C8, .C9, .C9, .CK, .CA]))
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [camiciaTests]
diff --git a/exercises/practice/camicia/lakefile.toml b/exercises/practice/camicia/lakefile.toml
new file mode 100644
index 0000000..5763bfc
--- /dev/null
+++ b/exercises/practice/camicia/lakefile.toml
@@ -0,0 +1,15 @@
+name = "camicia"
+version = "0.1.0"
+defaultTargets = ["CamiciaTest"]
+testDriver = "CamiciaTest"
+
+[[lean_lib]]
+name = "LeanTest"
+srcDir = "vendor/LeanTest"
+
+[[lean_lib]]
+name = "Camicia"
+
+[[lean_exe]]
+name = "CamiciaTest"
+root = "CamiciaTest"
diff --git a/exercises/practice/camicia/lean-toolchain b/exercises/practice/camicia/lean-toolchain
new file mode 100644
index 0000000..370b26d
--- /dev/null
+++ b/exercises/practice/camicia/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.25.2
diff --git a/exercises/practice/camicia/vendor/LeanTest/LeanTest.lean b/exercises/practice/camicia/vendor/LeanTest/LeanTest.lean
new file mode 100644
index 0000000..012ba20
--- /dev/null
+++ b/exercises/practice/camicia/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/camicia/vendor/LeanTest/LeanTest/Assertions.lean b/exercises/practice/camicia/vendor/LeanTest/LeanTest/Assertions.lean
new file mode 100644
index 0000000..60e4ad8
--- /dev/null
+++ b/exercises/practice/camicia/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/camicia/vendor/LeanTest/LeanTest/Test.lean b/exercises/practice/camicia/vendor/LeanTest/LeanTest/Test.lean
new file mode 100644
index 0000000..5ddbae5
--- /dev/null
+++ b/exercises/practice/camicia/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 cd25abb..f9868f6 100644
--- a/generators/Generator/Generator.lean
+++ b/generators/Generator/Generator.lean
@@ -1,3 +1,4 @@
+import Generator.CamiciaGenerator
 import Generator.YachtGenerator
 import Generator.PalindromeProductsGenerator
 import Generator.EtlGenerator
@@ -43,6 +44,7 @@ abbrev endBodyGenerator := String -> String
 
 def dispatch : Std.HashMap String (introGenerator × testCaseGenerator × endBodyGenerator) :=
   Std.HashMap.ofList [
+    ("Camicia", (CamiciaGenerator.genIntro, CamiciaGenerator.genTestCase, CamiciaGenerator.genEnd)),
     ("Yacht", (YachtGenerator.genIntro, YachtGenerator.genTestCase, YachtGenerator.genEnd)),
     ("PalindromeProducts", (PalindromeProductsGenerator.genIntro, PalindromeProductsGenerator.genTestCase, PalindromeProductsGenerator.genEnd)),
     ("Etl", (EtlGenerator.genIntro, EtlGenerator.genTestCase, EtlGenerator.genEnd)),
diff --git a/generators/Generator/Generator/CamiciaGenerator.lean b/generators/Generator/Generator/CamiciaGenerator.lean
new file mode 100644
index 0000000..e75deac
--- /dev/null
+++ b/generators/Generator/Generator/CamiciaGenerator.lean
@@ -0,0 +1,47 @@
+import Lean
+import Std
+import Helper
+
+open Lean
+open Std
+open Helper
+
+namespace CamiciaGenerator
+
+def genIntro (exercise : String) : String := s!"import LeanTest
+import {exercise}
+
+open LeanTest
+
+def {exercise.decapitalize}Tests : TestSuite :=
+  (TestSuite.empty \"{exercise}\")"
+
+def listOfCards (player : Json) : String :=
+  player.getArr? |> getOk
+    |>.map (λ j => toLiteral s!".C{j}")
+    |>.toList |> λ x => "[" ++ String.intercalate ", " x ++ "]"
+
+def genTestCase (exercise : String) (case : TreeMap.Raw String Json) : String :=
+  let input := case.get! "input"
+  let playerA := listOfCards (input.getObjValD "playerA")
+  let playerB := listOfCards (input.getObjValD "playerB")
+  let expected := case.get! "expected"
+  let status := toLiteral s!".{expected.getObjValD "status"}"
+  let cards := expected.getObjValD "cards"
+  let tricks := expected.getObjValD "tricks"
+  let description := case.get! "description"
+              |> (·.compress)
+  let funName := getFunName (case.get! "property")
+  let call := s!"({exercise}.{funName} {playerA} {playerB})"
+  s!"
+  |>.addTest {description} (do
+      return assertEqual ⟨{status}, {cards}, {tricks}⟩ {call})"
+
+def genEnd (exercise : String) : String :=
+  s!"
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [{exercise.decapitalize}Tests]
+"
+
+end CamiciaGenerator