diff --git a/HumanEvalLean/HumanEval78.lean b/HumanEvalLean/HumanEval78.lean
index 593460f..01c37fc 100644
--- a/HumanEvalLean/HumanEval78.lean
+++ b/HumanEvalLean/HumanEval78.lean
@@ -1,7 +1,27 @@
 module
+import Std
 
-def hex_key : Unit :=
-  ()
+open Std
+
+def primeList : List Char :=
+  ['2', '3', '5', '7', 'B', 'D']
+
+def primes : HashSet Char :=
+  .ofList primeList
+
+def hexKey (s : String) : Nat :=
+  s.chars.filter (· ∈ primes) |>.length
+
+example : hexKey "AB" = 1 := by native_decide
+example : hexKey "1077E" = 2 := by native_decide
+example : hexKey "ABED1A33" = 4 := by native_decide
+example : hexKey "2020" = 2 := by native_decide
+example : hexKey "123456789ABCDEF0" = 6 := by native_decide
+example : hexKey "112233445566778899AABBCCDDEEFF00" = 12 := by native_decide
+
+theorem hexKey_eq {s : String} : hexKey s = (s.toList.filter (· ∈ primeList)).length := by
+  rw [hexKey, ← Iter.length_toList_eq_length, primes]
+  simp
 
 /-!
 ## Prompt
@@ -9,15 +29,15 @@ def hex_key : Unit :=
 ```python3
 
 def hex_key(num):
-    """You have been tasked to write a function that receives 
-    a hexadecimal number as a string and counts the number of hexadecimal 
-    digits that are primes (prime number, or a prime, is a natural number 
+    """You have been tasked to write a function that receives
+    a hexadecimal number as a string and counts the number of hexadecimal
+    digits that are primes (prime number, or a prime, is a natural number
     greater than 1 that is not a product of two smaller natural numbers).
     Hexadecimal digits are 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, A, B, C, D, E, F.
     Prime numbers are 2, 3, 5, 7, 11, 13, 17,...
-    So you have to determine a number of the following digits: 2, 3, 5, 7, 
+    So you have to determine a number of the following digits: 2, 3, 5, 7,
     B (=decimal 11), D (=decimal 13).
-    Note: you may assume the input is always correct or empty string, 
+    Note: you may assume the input is always correct or empty string,
     and symbols A,B,C,D,E,F are always uppercase.
     Examples:
     For num = "AB" the output should be 1.
@@ -45,16 +65,16 @@ def hex_key(num):
 def check(candidate):
 
     # Check some simple cases
-    assert candidate("AB") == 1, "First test error: " + str(candidate("AB"))      
-    assert candidate("1077E") == 2, "Second test error: " + str(candidate("1077E"))  
-    assert candidate("ABED1A33") == 4, "Third test error: " + str(candidate("ABED1A33"))      
-    assert candidate("2020") == 2, "Fourth test error: " + str(candidate("2020"))  
-    assert candidate("123456789ABCDEF0") == 6, "Fifth test error: " + str(candidate("123456789ABCDEF0"))      
-    assert candidate("112233445566778899AABBCCDDEEFF00") == 12, "Sixth test error: " + str(candidate("112233445566778899AABBCCDDEEFF00"))  
+    assert candidate("AB") == 1, "First test error: " + str(candidate("AB"))
+    assert candidate("1077E") == 2, "Second test error: " + str(candidate("1077E"))
+    assert candidate("ABED1A33") == 4, "Third test error: " + str(candidate("ABED1A33"))
+    assert candidate("2020") == 2, "Fourth test error: " + str(candidate("2020"))
+    assert candidate("123456789ABCDEF0") == 6, "Fifth test error: " + str(candidate("123456789ABCDEF0"))
+    assert candidate("112233445566778899AABBCCDDEEFF00") == 12, "Sixth test error: " + str(candidate("112233445566778899AABBCCDDEEFF00"))
 
 
     # Check some edge cases that are easy to work out by hand.
     assert candidate([]) == 0
 
 ```
--/
\ No newline at end of file
+-/