LLM review: ask for literal Unicode so the mathematics is readable

python/lean_pool/review.py

@@ -290,6 +290,25 @@
 )
 
 
+# Appended to every system prompt. The first challenge review (PR #289)
+# came back with the mathematics unreadable: `over ^R09` for `over ℚ`,
+# `|(discr K : ^])| ^U 8.25 ^ finrank ^R0a K` for
+# `|(discr K : ℝ)| ≥ 8.25 ^ finrank ℚ K`. The mangling is the model's own —
+# nothing between `json.loads` and the posted comment touches those
+# strings — and it is not a systematic escape (`ℚ` came out as both `^R0a`
+# and `^R09`), so it cannot be decoded after the fact. Ask for the
+# characters directly, with a graceful fallback to words, since a review of
+# Lean that cannot render `ℚ` or `≥` is worth much less in this repository.
+NOTATION_RULE = dedent(
+    """\
+    Notation: when you quote Lean, copy the characters exactly as they
+    appear in the diff, Unicode included (ℚ, ℝ, ℕ, ≤, ≥, ∀, ∃, ⁄, ₀).
+    Never transliterate, escape, or approximate them. If you cannot
+    reproduce a symbol faithfully, describe it in words instead — a
+    sentence is readable, a mangled glyph is not.
+    """
+)
+
 # Rules document and system prompt per PR kind, keyed by `classify_pr`.
 REVIEW_MODES: dict[str, tuple[Path, str]] = {
     "project": (PROJECT_RULES_PATH, SYSTEM_PROMPT_PROJECT),
@@ -755,6 +774,7 @@ def request_review(
         full diff was reviewed).
     """
     client = OpenAI(timeout=REQUEST_TIMEOUT_SECONDS)
+    system_prompt = f"{system_prompt}\n{NOTATION_RULE}"
     scaffold_tokens = estimate_tokens(rules) + estimate_tokens(system_prompt)
     diff_budget_tokens = MAX_INPUT_TOKENS - scaffold_tokens
     for attempt in range(REVIEW_FIT_ATTEMPTS):

python/tests/test_review.py

@@ -573,3 +573,53 @@ def test_render_comment_notes_truncation() -> None:
     assert "Partial review" in body
     assert "250" in body and "317" in body
     assert "3,112,190" in body
+
+
+def test_every_review_mode_asks_for_literal_unicode(monkeypatch) -> None:
+    """The notation rule reaches the model whichever mode is reviewing.
+
+    PR #289's challenge review came back with `over ^R09` where `over ℚ`
+    belonged, so a Lean review that cannot render its own notation is a
+    regression worth a test.
+    """
+    from lean_pool import review
+
+    captured: list[dict] = []
+
+    class _Message:
+        content = '{"summary": "s", "verdict": "approve", "findings": []}'
+
+    class _Choice:
+        message = _Message()
+
+    class _Response:
+        choices = [_Choice()]
+        usage = None
+
+    class _Completions:
+        def create(self, **kwargs):
+            captured.append(kwargs)
+            return _Response()
+
+    class _Chat:
+        completions = _Completions()
+
+    class _Client:
+        chat = _Chat()
+
+        def __init__(self, **kwargs):
+            pass
+
+    monkeypatch.setattr(review, "OpenAI", _Client)
+
+    for _rules_path, system_prompt in review.REVIEW_MODES.values():
+        captured.clear()
+        review.request_review(
+            model="gpt-5.5",
+            rules="rules",
+            diff="diff --git a/A b/A",
+            system_prompt=system_prompt,
+        )
+        sent = captured[0]["messages"][0]["content"]
+        assert "copy the characters exactly" in sent
+        assert "ℚ" in sent