From 1bb8053f3a072c116bf6f019ac73f6d8cc8af13f Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Tue, 24 Mar 2026 10:52:46 +0000
Subject: [PATCH 1/2] 44

---
 HumanEvalLean/HumanEval44.lean | 24 +++++++++++++++++++++---
 1 file changed, 21 insertions(+), 3 deletions(-)

diff --git a/HumanEvalLean/HumanEval44.lean b/HumanEvalLean/HumanEval44.lean
index 1dce700..b203b87 100644
--- a/HumanEvalLean/HumanEval44.lean
+++ b/HumanEvalLean/HumanEval44.lean
@@ -1,7 +1,25 @@
 module
 
-def change_base : Unit :=
-  ()
+def changeBase (x : Nat) (base : Nat) : String :=
+  String.ofList (Nat.toDigits base x)
+
+example : changeBase 8 3 = "22" := by native_decide
+example : changeBase 9 3 = "100" := by native_decide
+example : changeBase 234 2 = "11101010" := by native_decide
+example : changeBase 16 2 = "10000" := by native_decide
+example : changeBase 8 2 = "1000" := by native_decide
+example : changeBase 7 2 = "111" := by native_decide
+
+namespace Nat
+
+theorem ofDigitChars_toDigits' {b n : Nat} (hb' : 1 < b) (hb : b ≤ 10) : ofDigitChars b (toDigits b n) 0 = n := by
+  sorry -- https://github.com/leanprover/lean4/pull/13098
+
+end Nat
+
+theorem ofDigitChars_changeBase {x : Nat} {base : Nat} (hb' : 1 < base) (hb : base ≤ 10) :
+    Nat.ofDigitChars base (changeBase x base).toList 0 = x := by
+  simp [changeBase, Nat.ofDigitChars_toDigits' hb' hb]
 
 /-!
 ## Prompt
@@ -51,4 +69,4 @@ def check(candidate):
         assert candidate(x, x + 1) == str(x)
 
 ```
--/
\ No newline at end of file
+-/

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

---
 HumanEvalLean/HumanEval44.lean | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/HumanEvalLean/HumanEval44.lean b/HumanEvalLean/HumanEval44.lean
index b203b87..46b8fe2 100644
--- a/HumanEvalLean/HumanEval44.lean
+++ b/HumanEvalLean/HumanEval44.lean
@@ -10,16 +10,9 @@ example : changeBase 16 2 = "10000" := by native_decide
 example : changeBase 8 2 = "1000" := by native_decide
 example : changeBase 7 2 = "111" := by native_decide
 
-namespace Nat
-
-theorem ofDigitChars_toDigits' {b n : Nat} (hb' : 1 < b) (hb : b ≤ 10) : ofDigitChars b (toDigits b n) 0 = n := by
-  sorry -- https://github.com/leanprover/lean4/pull/13098
-
-end Nat
-
 theorem ofDigitChars_changeBase {x : Nat} {base : Nat} (hb' : 1 < base) (hb : base ≤ 10) :
     Nat.ofDigitChars base (changeBase x base).toList 0 = x := by
-  simp [changeBase, Nat.ofDigitChars_toDigits' hb' hb]
+  simp [changeBase, Nat.ofDigitChars_toDigits hb' hb]
 
 /-!
 ## Prompt