Don't render a prior-art hedge as a confirmed duplicate

[Vilin97]

Follow-up to #293, from watching its first production run.

The review of #285 came back approve — and with this row in the table:

Aspect	Value
Already formalized	🛑 unverifiable from the supplied diff

The model answered the prior-art question in a field specified to hold a declaration name or nothing, and the renderer stamped 🛑 on whatever it found. So a PR the review approved carries a red row reading "this is a duplicate", which is the opposite of what the review concluded — and prior art is a request_changes ground, so that row is not cosmetic.

Two changes:

• _prior_art_cell renders a multi-word value as 🟡 <text> and keeps 🛑 \Decl.name`for an actual hit. The challenge renderer had the same latent bug — it has always used the identical🛑` line — and now shares the helper.
• Both rules docs tell the model the field is a bare declaration name, to leave it empty when it found nothing or could not check, and never to use it to say the question is unverifiable. source_match already has an unverifiable value for that.

Worth noting the run was otherwise exactly what the audit was after: it checked the Lean against the card and quoted the declaration, confirmed nothing substantive was postulated, named the disclosed hypothesis, and marked the source unverifiable instead of rubber-stamping it. Input rose 12,853 → 16,661 tokens, which is the PR description arriving for the first time.

🤖 Generated with Claude Code

[greptile-apps]

Greptile Summary

This PR fixes a rendering bug where a prose hedge returned by the LLM in the already_formalized field (e.g. "unverifiable from the supplied diff") was stamped with the same 🛑 icon used for an actual confirmed duplicate declaration name, misleadingly flagging an approved PR as prior art. It also updates both rules documents to instruct the model to leave the field empty rather than write explanatory prose.

• _prior_art_cell now distinguishes a single-word declaration name (🛑 Decl.name) from a multi-word prose response (🟡 text), and is shared between render_project_assessment and render_challenge_assessment, eliminating the same latent bug from the challenge renderer.
• Both REVIEW_RULES.md and CHALLENGE_REVIEW_RULES.md tighten the field specification to a bare declaration name and instruct the model never to write a sentence or "unverifiable" there.
• A regression test covers the hedge case end-to-end through render_project_assessment.

Confidence Score: 5/5

Safe to merge — the change is a targeted rendering fix with a direct regression test and no effect on any data-writing or decision-making path.

The fix is narrowly scoped: a new private helper function, two one-line call-site swaps, and two rule-doc clarifications. The heuristic (space in value → prose hedge, no space → declaration name) is sound for Lean 4 identifiers, which never contain spaces. The new test directly encodes the production failure mode that motivated the PR. No existing tests were removed or weakened.

Files Needing Attention: No files require special attention.

Important Files Changed

Filename	Overview
python/lean_pool/review.py	Extracts _prior_art_cell helper that gates on space presence to distinguish a declaration name from prose; both render_project_assessment and render_challenge_assessment now use it.
python/tests/test_review.py	Adds test_prior_art_hedge_is_not_rendered_as_a_duplicate covering both the hedge (🟡) and the declaration-name hit (🛑) paths through render_project_assessment.
.github/REVIEW_RULES.md	Tightens already_formalized field description to a bare declaration name and explicitly forbids writing a sentence or using it to report unverifiability.
.github/CHALLENGE_REVIEW_RULES.md	Applies the same already_formalized field-instruction tightening as REVIEW_RULES.md, mirroring the fix symmetrically for the challenge review path.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
    A["already_formalized field value"] --> B{value is non-empty?}
    B -- No --> C["Row omitted entirely"]
    B -- Yes --> D["_prior_art_cell(value)"]
    D --> E{"contains a space?"}
    E -- "Yes (prose/hedge)" --> F["🟡 text\n(no stop signal)"]
    E -- "No (bare declaration name)" --> G["🛑 \`Decl.name\`\n(confirmed duplicate)"]
    F --> H["render_project_assessment\nor render_challenge_assessment"]
    G --> H

Loading

_{Reviews (1): Last reviewed commit: "Don't render a prior-art hedge as a conf..." | Re-trigger Greptile}