diff --git a/HumanEvalLean/HumanEval64.lean b/HumanEvalLean/HumanEval64.lean
index 3b5b4d5..2f62633 100644
--- a/HumanEvalLean/HumanEval64.lean
+++ b/HumanEvalLean/HumanEval64.lean
@@ -1,7 +1,35 @@
 module
+import Std
 
-def vowels_count : Unit :=
-  ()
+open Std
+
+def vowelsList : List Char :=
+  ['a', 'e', 'i', 'o', 'u', 'A', 'E', 'I', 'O', 'U']
+
+def vowels : HashSet Char :=
+  .ofList vowelsList
+
+def vowelsCount (s : String) : Nat :=
+  let nVowels := s.chars.filter (· ∈ vowels) |>.length
+  let atEnd := if s.back?.any (fun c => c == 'y' || c == 'Y') then 1 else 0
+  nVowels + atEnd
+
+example : vowelsCount "abcde" = 2 := by native_decide
+example : vowelsCount "Alone" = 3 := by native_decide
+example : vowelsCount "key" = 2 := by native_decide
+example : vowelsCount "bye" = 1 := by native_decide
+example : vowelsCount "keY" = 2 := by native_decide
+example : vowelsCount "bYe" = 1 := by native_decide
+example : vowelsCount "ACEDY" = 3 := by native_decide
+
+theorem vowelsCount_eq {s : String} :
+    vowelsCount s = (s.toList.filter (· ∈ vowelsList)).length +
+      (if s.toList.getLast? = some 'y' ∨ s.toList.getLast? = some 'Y' then 1 else 0) := by
+  simp only [vowelsCount, ne_eq, ← Iter.length_toList_eq_length,
+    Iter.toList_filter, String.toList_chars, ↓Char.isValue]
+  simp only [vowels, HashSet.mem_ofList, List.contains_eq_mem, decide_eq_true_eq, ↓Char.isValue,
+    Option.any_eq_true, Bool.or_eq_true, beq_iff_eq, Nat.add_left_cancel_iff]
+  simp [and_comm, String.back?_eq]
 
 /-!
 ## Prompt
@@ -54,4 +82,4 @@ def check(candidate):
     assert True, "This prints if this assert fails 2 (also good for debugging!)"
 
 ```
--/
\ No newline at end of file
+-/