diff --git a/5-Applications/tools-scripts/llm/deepseek_v4_flash_lean_harness.py b/5-Applications/tools-scripts/llm/deepseek_v4_flash_lean_harness.py
index 33341201..f2ba7012 100644
--- a/5-Applications/tools-scripts/llm/deepseek_v4_flash_lean_harness.py
+++ b/5-Applications/tools-scripts/llm/deepseek_v4_flash_lean_harness.py
@@ -315,21 +315,35 @@ def extract_errors(log: str) -> str:
 
 
 def extract_proof_code(response: str) -> str:
-    text = re.sub(r"^\s*```(?:lean)?\s*\n?", "", response, flags=re.MULTILINE)
-    text = re.sub(r"\n\s*```\s*$", "", text, flags=re.MULTILINE)
-    text = text.strip()
-
-    if text.startswith(":= by"):
-        return text
+    # 1. Try to extract content inside markdown code blocks first to ignore explanations
+    blocks = re.findall(r"```(?:lean)?\n(.*?)\n```", response, re.DOTALL | re.IGNORECASE)
+    if blocks:
+        text = blocks[-1].strip()
+    else:
+        # Fallback to manual stripping if markdown block is unclosed or malformed
+        text = re.sub(r"^\s*```(?:lean)?\s*\n?", "", response, flags=re.MULTILINE)
+        text = re.sub(r"\n\s*```\s*$", "", text, flags=re.MULTILINE)
+        text = text.strip()
 
+    # 2. Extract proof body matching case variations to prevent formatting drift failures:
+    # Case A: Contains ":= by"
     idx = text.find(":= by")
     if idx >= 0:
         return text[idx:]
 
-    idx = text.find("\nby ")
-    if idx >= 0:
-        prev_newline = text.rfind("\n", 0, idx)
-        return text[prev_newline + 1:].strip()
+    # Case B: Contains ":=" followed by optional space/newline and then "by"
+    m = re.search(r":=\s*(by\b.*)", text, re.DOTALL)
+    if m:
+        return ":= " + m.group(1)
+
+    # Case C: Starts with "by"
+    if text.startswith("by\n") or text.startswith("by "):
+        return text
+    
+    # Case D: Contains a line starting with "by "
+    m = re.search(r"(?:\n|^)\s*(by\b.*)", text, re.DOTALL)
+    if m:
+        return m.group(1)
 
     return text
 
@@ -371,6 +385,20 @@ def insert_proof(lean_path: Path, sorry_line: int, proof_code: str) -> bool:
     if code.startswith(":= by"):
         code = code[5:].strip()
 
+    # Avoid duplicate "by by" syntax errors if insertion point already has "by"
+    insertion_line = lines[insert_idx]
+    has_by = "by" in insertion_line or (insert_idx > 0 and "by" in lines[insert_idx - 1])
+    
+    if has_by:
+        if code.startswith("by "):
+            code = code[3:].strip()
+        elif code.startswith("by\n"):
+            code = code[2:].strip()
+    else:
+        # Ensure code starts with "by" if insertion point is missing it
+        if not code.startswith("by\n") and not code.startswith("by "):
+            code = "by\n  " + code
+
     # Build indented proof lines (preserve blank lines).
     proof_lines: list[str] = []
     for pl in code.split("\n"):