Preserve mathematical backslashes in reviewer JSON

python/lean_pool/codex_review.py

@@ -9,6 +9,7 @@
 
 import json
 import os
+import re
 import signal
 import subprocess
 import sys
@@ -195,7 +196,7 @@ def run_codex(request: dict, directory: Path) -> dict:
     if process.returncode:
         raise RuntimeError(f"Codex exited {process.returncode}: {stderr[-2000:]}")
     envelope = json.loads((directory / "answer.json").read_text())
-    payload = json.loads(envelope["review_json"])
+    payload = decode_review_json(envelope["review_json"])
     if not isinstance(payload, dict) or not payload:
         raise ValueError("Codex did not return a review object")
     usage = extract_usage(stdout)
@@ -207,6 +208,22 @@ def run_codex(request: dict, directory: Path) -> dict:
     }
 
 
+def decode_review_json(source: str) -> Any:
+    """Preserve literal Lean/LaTeX backslashes in otherwise valid model JSON."""
+    try:
+        return json.loads(source)
+    except json.JSONDecodeError as error:
+        if error.msg != "Invalid \\escape":
+            raise
+    # Consume valid escape pairs intact, including already escaped backslashes.
+    repaired = re.sub(
+        r'\\(?:["\\/bfnrtu]|([^"\\/bfnrtu]))',
+        lambda match: "\\\\" + match[1] if match[1] else match[0],
+        source,
+    )
+    return json.loads(repaired)
+
+
 def stop_codex(process: subprocess.Popen) -> None:
     """Let the account dispatcher forward termination to its separate child group."""
     try:

python/tests/test_codex_review.py

@@ -256,3 +256,31 @@ def test_azure_partial_usage_labels_partial_estimate():
     )
     assert "**Estimated cost:** $1.0500" in footer
     assert "partial" in footer
+
+
+def test_review_json_preserves_literal_mathematical_backslashes():
+    """An invalid JSON escape must not lose completed mathematical evidence."""
+    raw = (
+        r'{"verdict":"discuss","evidence":"\lambda x => x; '
+        r'\\proper; \nline; \"quote\"; \set"}'
+    )
+    result = codex_review.decode_review_json(raw)
+    assert result == {
+        "verdict": "discuss",
+        "evidence": '\\lambda x => x; \\proper; \nline; "quote"; \\set',
+    }
+
+
+@pytest.mark.parametrize(
+    "source", [r'{"evidence":"\u123"}', '{"verdict":"pass"', r'{"x":\broken}']
+)
+def test_review_json_other_malformed_output_still_fails(source):
+    """Backslash handling cannot invent missing structure or repair other errors."""
+    with pytest.raises(json.JSONDecodeError):
+        codex_review.decode_review_json(source)
+
+
+def test_valid_review_json_is_unchanged():
+    """Valid escapes and Unicode keep their ordinary JSON meanings."""
+    payload = {"verdict": "pass", "evidence": '\\lambda\n"quoted"\tλ'}
+    assert codex_review.decode_review_json(json.dumps(payload)) == payload