From 6cd9e63af3089a33a5e3aacde1170d0c90a92aff Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Tue, 28 Jul 2026 01:19:40 -0700 Subject: [PATCH] The first challenge review ([#289](https://github.com/Vilin97/lean-pool/pull/289)) came back with the mathematics unreadable: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit > elliptic curves over `^R09` … `|(discr K : ^])| ^U 8.25 ^ finrank ^R0a K` where it should read `over ℚ` and `|(discr K : ℝ)| ≥ 8.25 ^ finrank ℚ K`. The mangling is the model's own: nothing between `json.loads` and the posted comment touches those strings, the bytes in the stored comment are literal ASCII, and Greptile's comment through the same fetch path renders `ℚ` fine. It is also not a systematic escape — `ℚ` came out as `^R0a` in three places and `^R09` in another — so it cannot be decoded after the fact, only prevented. So: one notation rule, appended to every system prompt, asking for the characters as they appear in the diff and offering a graceful fallback (describe the symbol in words) rather than an approximation. A review of Lean that cannot render `ℚ` or `≥` is worth much less in this repository. Tested by asserting the rule reaches the model for every mode in `REVIEW_MODES`, so a new review kind cannot quietly skip it. Verified for real by re-running `/review` on #289 after this merges. 🤖 Generated with [Claude Code](https://claude.com/claude-code) BODY LLM review: ask for literal Unicode so the mathematics is readable The first challenge review (#289) came back with the mathematics unreadable: `over ^R09` for `over ℚ`, and `|(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, the stored bytes are literal ASCII, and another bot's comment through the same fetch path renders `ℚ` fine. It is not a systematic escape either (`ℚ` came out as both `^R0a` and `^R09`), so it cannot be decoded after the fact, only prevented. Append one notation rule to every system prompt: copy the characters as they appear in the diff, and if a symbol cannot be reproduced, describe it in words rather than approximate it. A test asserts the rule reaches the model for every mode in REVIEW_MODES. Co-Authored-By: Claude Opus 5 --- python/lean_pool/review.py | 20 +++++++++++++++ python/tests/test_review.py | 50 +++++++++++++++++++++++++++++++++++++ 2 files changed, 70 insertions(+) diff --git a/python/lean_pool/review.py b/python/lean_pool/review.py index fa3cc988d5..406ea2ba54 100644 --- a/python/lean_pool/review.py +++ b/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): diff --git a/python/tests/test_review.py b/python/tests/test_review.py index b05b383528..22585eb05d 100644 --- a/python/tests/test_review.py +++ b/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