diff --git a/src/lean4/human_eval/problem_103.lean b/src/lean4/human_eval/problem_103.lean
index 16c191b..37cc1d8 100644
--- a/src/lean4/human_eval/problem_103.lean
+++ b/src/lean4/human_eval/problem_103.lean
@@ -82,7 +82,7 @@ else
 -- #test implementation 7 13 = some "0b1010"
 -- #test implementation 964 977 = some "0b1111001010"
 -- #test implementation 996 997 = some "0b1111100100"
--- #test implementation 185 546 = some "0b101101110"
+-- #test implementation 185 546 = some "0b101101101"
 -- #test implementation 362 496 = some "0b110101101"
 -- #test implementation 350 902 = some "0b1001110010"
 -- #test implementation 197 233 = some "0b11010111"
diff --git a/src/lean4/sample_examples/problem_1.lean b/src/lean4/sample_examples/problem_1.lean
index 5b7644f..2dfc690 100644
--- a/src/lean4/sample_examples/problem_1.lean
+++ b/src/lean4/sample_examples/problem_1.lean
@@ -413,7 +413,7 @@ linarith
 theorem spec_isomorphism:
 ∀ impl,
 (∀ score_changes threshold, problem_spec impl score_changes threshold) ↔
-(∀ score_changes threshold, generated_spec impl score_changes threshold) := by
+(∀ score_changes threshold, generated_spec impl score_changes threshold) :=
 -- end_def spec_isomorphism
 -- start_def spec_isomorphism_proof
 sorry
diff --git a/src/lean4/sample_examples/problem_3.lean b/src/lean4/sample_examples/problem_3.lean
index e8b8ff0..9c00ebf 100644
--- a/src/lean4/sample_examples/problem_3.lean
+++ b/src/lean4/sample_examples/problem_3.lean
@@ -53,6 +53,8 @@ def generated_spec
 (impl: Nat → Nat)
 -- inputs
 (n: Nat) : Prop :=
+--end_def generated_spec
+--start_def generated_spec_body
 -- spec
 let spec (result: Nat) :=
 match n with
@@ -62,7 +64,7 @@ match n with
 -- return value satisfies spec
 ∃ result, impl n = result ∧
 spec result
--- end_def generated_spec
+-- end_def generated_spec_body
 
 -- start_def iso_helper_lemmas
 lemma fib0_unique (n : ℕ) (h : fibonacci_non_computable 0 n) : n = 0 :=
diff --git a/src/lean4/sample_examples/problem_5.lean b/src/lean4/sample_examples/problem_5.lean
index 9d87c71..b6a6ab9 100644
--- a/src/lean4/sample_examples/problem_5.lean
+++ b/src/lean4/sample_examples/problem_5.lean
@@ -50,9 +50,11 @@ def generated_spec
 (impl: Nat → Nat)
 -- inputs
 (n: Nat) : Prop :=
+--end_def generated_spec
+--start_def generated_spec_body
 -- spec
 sorry
--- end_def generated_spec
+-- end_def generated_spec_body
 
 -- start_def spec_isomorphism
 theorem spec_isomorphism: