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

[Vilin97]

No description provided.

[greptile-apps]

Greptile Summary

This PR appends a NOTATION_RULE constant to every LLM system prompt in request_review, instructing the model to reproduce Lean Unicode symbols (ℚ, ℝ, ≥, etc.) verbatim rather than mangling them. A companion test verifies the rule is injected for all REVIEW_MODES.

• review.py: Adds NOTATION_RULE (with a clear inline comment explaining the regression in PR Challenges: Odlyzko root-discriminant bound and Mazur's torsion bound #289) and appends it to system_prompt before the token-budget calculation, so the enlarged prompt is correctly accounted for in scaffold_tokens.
• test_review.py: Adds test_every_review_mode_asks_for_literal_unicode, which stubs the OpenAI client, iterates over all review modes, and asserts both the key phrase and a sample Unicode character are present in the transmitted system message.

Confidence Score: 5/5

The change is a narrow, targeted addition: one new string constant appended to every system prompt, with correct token-budget accounting and a well-scoped test.

Both changed files are straightforward. The notation rule is appended before scaffold_tokens is computed, so the enlarged prompt is correctly reflected in the diff budget. The test stubs the OpenAI client and exercises all review modes, giving good confidence the rule will reach the model in production.

Files Needing Attention: No files require special attention.

Important Files Changed

Filename	Overview
python/lean_pool/review.py	Adds NOTATION_RULE constant and appends it to the system prompt before token budgeting — straightforward and correct.
python/tests/test_review.py	Adds a test that stubs OpenAI, exercises every REVIEW_MODE, and checks the notation rule reaches the system message — good coverage.

_{Reviews (1): Last reviewed commit: "The first challenge review ([#289](https..." | Re-trigger Greptile}