diff --git a/HumanEvalLean/HumanEval84.lean b/HumanEvalLean/HumanEval84.lean
index fbb440b..d681e5e 100644
--- a/HumanEvalLean/HumanEval84.lean
+++ b/HumanEvalLean/HumanEval84.lean
@@ -1,7 +1,19 @@
 module
 
-def solve : Unit :=
-  ()
+def solve (n : Nat) : String :=
+  String.ofList (Nat.toDigits 2 (n.repr.chars.map (fun c => c.toNat - '0'.toNat) |>.fold (init := 0) (· + ·)))
+
+example : solve 1000 = "1" := by native_decide
+example : solve 150 = "110" := by native_decide
+example : solve 147 = "1100" := by native_decide
+example : solve 333 = "1001" := by native_decide
+example : solve 963 = "10010" := by native_decide
+
+theorem ofDigitChars_solve {n : Nat} :
+    Nat.ofDigitChars 2 (solve n).toList 0 = (n.repr.toList.map (fun c => c.toNat - '0'.toNat)).sum := by
+  rw [solve, String.toList_ofList, Nat.ofDigitChars_toDigits (by simp) (by simp),
+    ← Std.Iter.foldl_toList, Std.Iter.toList_map]
+  simp [List.sum_eq_foldl]
 
 /-!
 ## Prompt
@@ -10,12 +22,12 @@ def solve : Unit :=
 
 def solve(N):
     """Given a positive integer N, return the total sum of its digits in binary.
-    
+
     Example
         For N = 1000, the sum of digits will be 1 the output should be "1".
         For N = 150, the sum of digits will be 6 the output should be "110".
         For N = 147, the sum of digits will be 12 the output should be "1100".
-    
+
     Variables:
         @N integer
              Constraints: 0 ≤ N ≤ 10000.
@@ -47,4 +59,4 @@ def check(candidate):
     assert candidate(963) == "10010", "Error"
 
 ```
--/
\ No newline at end of file
+-/