exercism · oxe-i · Feb 22, 2026 · Feb 22, 2026
diff --git a/exercises/practice/acronym/Acronym.lean b/exercises/practice/acronym/Acronym.lean
@@ -1,6 +1,6 @@
 namespace Acronym
 
 def abbreviate (phrase : String) : String :=
-  sorry
+  sorry --remove this line and implement the function
 
 end Acronym
diff --git a/exercises/practice/affine-cipher/AffineCipher.lean b/exercises/practice/affine-cipher/AffineCipher.lean
@@ -1,9 +1,9 @@
 namespace AffineCipher
 
 def encode (phrase : String) (a : Nat) (b : Nat) : Option String :=
-  sorry
+  sorry --remove this line and implement the function
 
 def decode (phrase : String) (a : Nat) (b : Nat) : Option String :=
-  sorry
+  sorry --remove this line and implement the function
 
 end AffineCipher
diff --git a/exercises/practice/all-your-base/AllYourBase.lean b/exercises/practice/all-your-base/AllYourBase.lean
@@ -3,6 +3,6 @@ namespace AllYourBase
 def ValidBase := { x : Nat // x >= 2 }
 
 def rebase (inputBase : ValidBase) (digits : List (Fin inputBase.val)) (outputBase : ValidBase) : List (Fin outputBase.val) :=
-  sorry
+  sorry --remove this line and implement the function
 
 end AllYourBase
diff --git a/exercises/practice/allergies/Allergies.lean b/exercises/practice/allergies/Allergies.lean
@@ -12,9 +12,9 @@ inductive Allergen where
   deriving BEq, Repr
 
 def allergicTo (allergen : Allergen) (score : Nat) : Bool :=
-  sorry
+  sorry --remove this line and implement the function
 
 def list (score : Nat) : List Allergen :=
-  sorry
+  sorry --remove this line and implement the function
 
 end Allergies
diff --git a/exercises/practice/anagram/Anagram.lean b/exercises/practice/anagram/Anagram.lean
@@ -1,6 +1,6 @@
 namespace Anagram
 
 def findAnagrams (subject : String) : List String -> List String :=
-  sorry
+  sorry --remove this line and implement the function
 
 end Anagram
diff --git a/exercises/practice/armstrong-numbers/ArmstrongNumbers.lean b/exercises/practice/armstrong-numbers/ArmstrongNumbers.lean
@@ -1,6 +1,6 @@
 namespace ArmstrongNumbers
 
 def isArmstrongNumber (number : Nat) : Bool :=
-  sorry
+  sorry --remove this line and implement the function
 
 end ArmstrongNumbers
diff --git a/exercises/practice/atbash-cipher/AtbashCipher.lean b/exercises/practice/atbash-cipher/AtbashCipher.lean
@@ -1,9 +1,9 @@
 namespace AtbashCipher
 
 def encode (phrase : String) : String :=
-  sorry
+  sorry --remove this line and implement the function
 
 def decode (phrase : String) : String :=
-  sorry
+  sorry --remove this line and implement the function
 
 end AtbashCipher
diff --git a/exercises/practice/bank-account/BankAccount.lean b/exercises/practice/bank-account/BankAccount.lean
@@ -5,21 +5,21 @@ structure Account where
   -- it must be able to handle parallel transactions
 
 def Account.create : IO Account :=
-  sorry
+  sorry --remove this line and implement the function
 
 def Account.open (account : Account) : IO Unit :=
-  sorry
+  sorry --remove this line and implement the function
 
 def Account.close (account : Account) : IO Unit :=
-  sorry
+  sorry --remove this line and implement the function
 
 def Account.deposit (amount : Nat) (account : Account) : IO Unit :=
-  sorry
+  sorry --remove this line and implement the function
 
 def Account.withdraw (amount : Nat) (account : Account) : IO Unit :=
-  sorry
+  sorry --remove this line and implement the function
 
 def Account.balance (account : Account) : IO Nat :=
-  sorry
+  sorry --remove this line and implement the function
 
 end BankAccount
diff --git a/exercises/practice/binary-search/BinarySearch.lean b/exercises/practice/binary-search/BinarySearch.lean
@@ -1,6 +1,6 @@
 namespace BinarySearch
 
 def find (value : Int) (array : Array Int) : Option Nat :=
-  sorry
+  sorry --remove this line and implement the function
 
 end BinarySearch
diff --git a/exercises/practice/bob/Bob.lean b/exercises/practice/bob/Bob.lean
@@ -1,6 +1,6 @@
 namespace Bob
 
 def response (heyBob : String) : String :=
-  sorry
+  sorry --remove this line and implement the function
 
 end Bob
diff --git a/exercises/practice/book-store/BookStore.lean b/exercises/practice/book-store/BookStore.lean
@@ -3,6 +3,6 @@ namespace BookStore
 def Book := { x : Nat // x ≥ 1 ∧ x ≤ 5 }
 
 def total (basket : List Book) : Nat :=
-  sorry
+  sorry --remove this line and implement the function
 
 end BookStore
diff --git a/exercises/practice/camicia/Camicia.lean b/exercises/practice/camicia/Camicia.lean
@@ -16,6 +16,6 @@ structure Result where
   deriving BEq, Repr
 
 def simulateGame (playerA playerB : List Card) : Result :=
-  sorry
+  sorry --remove this line and implement the function
 
 end Camicia
diff --git a/exercises/practice/change/Change.lean b/exercises/practice/change/Change.lean
@@ -6,6 +6,6 @@ inductive Result where
   deriving BEq, Repr
 
 def findFewestCoins (coins : Array Nat) (target : Int) : Result :=
-  sorry
+  sorry --remove this line and implement the function
 
 end Change
diff --git a/exercises/practice/clock/Clock.lean b/exercises/practice/clock/Clock.lean
@@ -5,19 +5,21 @@ structure Clock where
 
 -- define equality between Clocks
 instance : BEq Clock where
-  beq clock1 clock2 := sorry
+  beq clock1 clock2 :=
+    sorry --remove this line and implement the function
 
 -- define how a Clock should be converted to a String
 instance : ToString Clock where
-  toString clock := sorry
+  toString clock :=
+    sorry --remove this line and implement the function
 
 def create (hour : Int) (minute : Int) : Clock :=
-  sorry
+  sorry --remove this line and implement the function
 
 def add (clock : Clock) (minute : Int) : Clock :=
-  sorry
+  sorry --remove this line and implement the function
 
 def subtract (clock : Clock) (minute : Int) : Clock :=
-  sorry
+  sorry --remove this line and implement the function
 
 end Clock
diff --git a/exercises/practice/collatz-conjecture/CollatzConjecture.lean b/exercises/practice/collatz-conjecture/CollatzConjecture.lean
@@ -3,6 +3,6 @@ namespace CollatzConjecture
 def Positive := { x : Nat // 0 < x }
 
 def steps (n : Positive) : Nat :=
-  sorry
+  sorry --remove this line and implement the function
 
 end CollatzConjecture
diff --git a/exercises/practice/complex-numbers/ComplexNumbers.lean b/exercises/practice/complex-numbers/ComplexNumbers.lean
@@ -7,33 +7,34 @@ structure ComplexNumber where
 
 /- define how a complex number should be constructed out of a literal number -/
 instance {n : Nat} : OfNat ComplexNumber n where
-  ofNat := sorry
+  ofNat :=
+    sorry --remove this line and implement the function
 
 def real (z : ComplexNumber) : Float :=
-  sorry
+  sorry --remove this line and implement the function
 
 def imaginary (z : ComplexNumber) : Float :=
-  sorry
+  sorry --remove this line and implement the function
 
 def mul (z1 : ComplexNumber) (z2 : ComplexNumber) : ComplexNumber :=
-  sorry
+  sorry --remove this line and implement the function
 
 def div (z1 : ComplexNumber) (z2 : ComplexNumber) : ComplexNumber :=
-  sorry
+  sorry --remove this line and implement the function
 
 def sub (z1 : ComplexNumber) (z2 : ComplexNumber) : ComplexNumber :=
-  sorry
+  sorry --remove this line and implement the function
 
 def add (z1 : ComplexNumber) (z2 : ComplexNumber) : ComplexNumber :=
-  sorry
+  sorry --remove this line and implement the function
 
 def abs (z : ComplexNumber) : Float :=
-  sorry
+  sorry --remove this line and implement the function
 
 def conjugate (z : ComplexNumber) : ComplexNumber :=
-  sorry
+  sorry --remove this line and implement the function
 
 def exp (z : ComplexNumber) : ComplexNumber :=
-  sorry
+  sorry --remove this line and implement the function
 
 end ComplexNumbers
diff --git a/exercises/practice/connect/Connect.lean b/exercises/practice/connect/Connect.lean
@@ -1,6 +1,6 @@
 namespace Connect
 
 def winner (board : Array String) : Char :=
-  sorry
+  sorry --remove this line and implement the function
 
 end Connect
diff --git a/exercises/practice/crypto-square/CryptoSquare.lean b/exercises/practice/crypto-square/CryptoSquare.lean
@@ -1,6 +1,6 @@
 namespace CryptoSquare
 
 def ciphertext (plaintext : String) : String :=
-  sorry
+  sorry --remove this line and implement the function
 
 end CryptoSquare
diff --git a/exercises/practice/darts/Darts.lean b/exercises/practice/darts/Darts.lean
@@ -1,6 +1,6 @@
 namespace Darts
 
 def score (x : Float) (y : Float) : Int :=
-  sorry
+  sorry --remove this line and implement the function
 
 end Darts
diff --git a/exercises/practice/diamond/Diamond.lean b/exercises/practice/diamond/Diamond.lean
@@ -1,6 +1,6 @@
 namespace Diamond
 
 def rows (letter : Char) : List String :=
-  sorry
+  sorry --remove this line and implement the function
 
 end Diamond
diff --git a/exercises/practice/difference-of-squares/DifferenceOfSquares.lean b/exercises/practice/difference-of-squares/DifferenceOfSquares.lean
@@ -1,12 +1,12 @@
 namespace DifferenceOfSquares
 
 def squareOfSum (number : Nat) : Nat :=
-  sorry
+  sorry --remove this line and implement the function
 
 def sumOfSquares (number : Nat) : Nat :=
-  sorry
+  sorry --remove this line and implement the function
 
 def differenceOfSquares (number : Nat) : Nat :=
-  sorry
+  sorry --remove this line and implement the function
 
 end DifferenceOfSquares
diff --git a/exercises/practice/dnd-character/DndCharacter.lean b/exercises/practice/dnd-character/DndCharacter.lean
@@ -10,12 +10,12 @@ structure Character where
   hitpoints    : Int
 
 def modifier (score : Nat) : Int :=
-  sorry
+  sorry --remove this line and implement the function
 
 def ability {α} [RandomGen α] (generator : α) : (Nat × α) :=
-  sorry
+  sorry --remove this line and implement the function
 
 def Character.new {α} [RandomGen α] (generator : α) : (Character × α) :=
-  sorry
+  sorry --remove this line and implement the function
 
 end DndCharacter
diff --git a/exercises/practice/dominoes/Dominoes.lean b/exercises/practice/dominoes/Dominoes.lean
@@ -5,6 +5,6 @@ def Half := { x : Nat // x ≥ 1 ∧ x ≤ 6 }
 def Stone := Half × Half
 
 def canChain (dominoes : List Stone) : Bool :=
-  sorry
+  sorry --remove this line and implement the function
 
 end Dominoes
diff --git a/exercises/practice/eliuds-eggs/EliudsEggs.lean b/exercises/practice/eliuds-eggs/EliudsEggs.lean
@@ -1,6 +1,6 @@
 namespace EliudsEggs
 
 def eggCount (number : Nat) : Nat :=
-  sorry
+  sorry --remove this line and implement the function
 
 end EliudsEggs
diff --git a/exercises/practice/etl/Etl.lean b/exercises/practice/etl/Etl.lean
@@ -3,6 +3,6 @@ import Std
 namespace Etl
 
 def transform (legacy : Std.HashMap Nat (List Char)) : Std.HashMap Char Nat :=
-  sorry
+  sorry --remove this line and implement the function
 
 end Etl
diff --git a/exercises/practice/flatten-array/FlattenArray.lean b/exercises/practice/flatten-array/FlattenArray.lean
@@ -6,6 +6,6 @@ inductive Box (α : Type) : Type where
   | many (boxes : Array (Box α))
 
 def flatten (box : Box Int) : Array Int :=
-  sorry
+  sorry --remove this line and implement the function
 
 end FlattenArray
diff --git a/exercises/practice/forth/Forth.lean b/exercises/practice/forth/Forth.lean
@@ -1,6 +1,6 @@
 namespace Forth
 
 def evaluate (instructions : List String) : Except String (List Int) :=
-  sorry
+  sorry --remove this line and implement the function
 
 end Forth
diff --git a/exercises/practice/game-of-life/GameOfLife.lean b/exercises/practice/game-of-life/GameOfLife.lean
@@ -1,6 +1,6 @@
 namespace GameOfLife
 
 def tick (matrix : Array (Array Bool)) : Array (Array Bool) :=
-  sorry
+  sorry --remove this line and implement the function
 
 end GameOfLife
diff --git a/exercises/practice/gigasecond/Gigasecond.lean b/exercises/practice/gigasecond/Gigasecond.lean
@@ -3,6 +3,6 @@ import Std.Time
 namespace Gigasecond
 
 def add (moment : Std.Time.PlainDateTime) : Std.Time.PlainDateTime :=
-  sorry
+  sorry --remove this line and implement the function
 
 end Gigasecond
diff --git a/exercises/practice/grains/Grains.lean b/exercises/practice/grains/Grains.lean
@@ -1,9 +1,9 @@
 namespace Grains
 
 def grains (square : Int) : Option Nat :=
-  sorry
+  sorry --remove this line and implement the function
 
 def totalGrains : Nat :=
-  sorry
+  sorry --remove this line and implement the function
 
 end Grains
diff --git a/exercises/practice/grep/Grep.lean b/exercises/practice/grep/Grep.lean
@@ -1,6 +1,6 @@
 namespace Grep
 
 def grep (args : List String) : IO Unit :=
-  sorry
+  sorry --remove this line and implement the function
 
 end Grep
diff --git a/exercises/practice/hamming/Hamming.lean b/exercises/practice/hamming/Hamming.lean
@@ -1,6 +1,6 @@
 namespace Hamming
 
 def distance (strand1 : String) (strand2 : String) : Option Nat :=
-  sorry
+  sorry --remove this line and implement the function
 
 end Hamming
diff --git a/exercises/practice/high-scores/HighScores.lean b/exercises/practice/high-scores/HighScores.lean
@@ -1,21 +1,21 @@
 namespace HighScores
 
 def latestList (scores : List Nat) : Nat :=
-  sorry
+  sorry --remove this line and implement the function
 
 def latestArray (scores : Array Nat) : Nat :=
-  sorry
+  sorry --remove this line and implement the function
 
 def personalBestList (scores : List Nat) : Nat :=
-  sorry
+  sorry --remove this line and implement the function
 
 def personalBestArray (scores : Array Nat) : Nat :=
-  sorry
+  sorry --remove this line and implement the function
 
 def personalTopThreeList (scores : List Nat) : List Nat :=
-  sorry
+  sorry --remove this line and implement the function
 
 def personalTopThreeArray (scores : Array Nat) : Array Nat :=
-  sorry
+  sorry --remove this line and implement the function
 
 end HighScores
diff --git a/exercises/practice/house/House.lean b/exercises/practice/house/House.lean
@@ -3,6 +3,6 @@ namespace House
 abbrev VerseIndex := { x : Nat // 1 ≤ x ∧ x ≤ 12 }
 
 def recite (startVerse endVerse : VerseIndex) : String :=
-  sorry
+  sorry --remove this line and implement the function
 
 end House