From b3128f88ab7613c345edb6d81e90e1d72a829f77 Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Tue, 24 Mar 2026 14:27:35 +0000
Subject: [PATCH 1/2] 64

---
 HumanEvalLean/HumanEval64.lean | 37 +++++++++++++++++++++++++++++++---
 1 file changed, 34 insertions(+), 3 deletions(-)

diff --git a/HumanEvalLean/HumanEval64.lean b/HumanEvalLean/HumanEval64.lean
index 3b5b4d5..53d1310 100644
--- a/HumanEvalLean/HumanEval64.lean
+++ b/HumanEvalLean/HumanEval64.lean
@@ -1,7 +1,38 @@
 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 String.back?_eq {s : String} : s.back? = s.toList.getLast? :=
+  sorry -- https://github.com/leanprover/lean4/pull/13105
+
+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 +85,4 @@ def check(candidate):
     assert True, "This prints if this assert fails 2 (also good for debugging!)"
 
 ```
--/
\ No newline at end of file
+-/

From 1785677206232d0a08ad94462441ef6c71a04b5b Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Thu, 26 Mar 2026 08:21:36 +0000
Subject: [PATCH 2/2] Fix

---
 HumanEvalLean/HumanEval64.lean | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/HumanEvalLean/HumanEval64.lean b/HumanEvalLean/HumanEval64.lean
index 53d1310..2f62633 100644
--- a/HumanEvalLean/HumanEval64.lean
+++ b/HumanEvalLean/HumanEval64.lean
@@ -22,9 +22,6 @@ example : vowelsCount "keY" = 2 := by native_decide
 example : vowelsCount "bYe" = 1 := by native_decide
 example : vowelsCount "ACEDY" = 3 := by native_decide
 
-theorem String.back?_eq {s : String} : s.back? = s.toList.getLast? :=
-  sorry -- https://github.com/leanprover/lean4/pull/13105
-
 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