From ea56d7381956914aad28767334ff6221288834ed Mon Sep 17 00:00:00 2001
From: Vasily Ilin <vasilin97@gmail.com>
Date: Tue, 28 Jul 2026 22:45:34 -0700
Subject: [PATCH] Don't render a prior-art hedge as a confirmed duplicate
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The first production run under the audited rules answered
`already_formalized` with "unverifiable from the supplied diff" — prose,
in a field specified as a declaration name — and the renderer stamped 🛑
on it. On a PR the same review approved, that row read as "this is a
duplicate", the opposite of what the review said.

Render a multi-word answer as the hedge it is, and tell both rules docs
to leave the field empty rather than answering the question in it. The
challenge renderer had the same latent bug and goes through the same
helper now.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 .github/CHALLENGE_REVIEW_RULES.md |  2 +-
 .github/REVIEW_RULES.md           |  2 +-
 python/lean_pool/review.py        | 19 +++++++++++++++++--
 python/tests/test_review.py       | 21 +++++++++++++++++++++
 4 files changed, 40 insertions(+), 4 deletions(-)

diff --git a/.github/CHALLENGE_REVIEW_RULES.md b/.github/CHALLENGE_REVIEW_RULES.md
index 40c2498617..ea6509e5f2 100644
--- a/.github/CHALLENGE_REVIEW_RULES.md
+++ b/.github/CHALLENGE_REVIEW_RULES.md
@@ -126,7 +126,7 @@ Return a single JSON object:
     "difficulty": "exercise" | "substantial" | "research" | "open_problem",
     "estimated_lines": <int: lines of Lean a solution would take>,
     "estimate_basis": "<one sentence: what the estimate rests on>",
-    "already_formalized": "<Mathlib or pool declaration that already proves this, or empty>",
+    "already_formalized": "<the Mathlib or pool declaration that already proves this — a bare declaration name and nothing else. Leave EMPTY if you found none or could not check; do not write a sentence here, and never use it to say the question is unverifiable>",
     "assessment_one_sentence": "<one sentence: the bottom line for the maintainer>"
   },
   "verdict": "approve" | "request_changes" | "needs_discussion",
diff --git a/.github/REVIEW_RULES.md b/.github/REVIEW_RULES.md
index f65a645c33..2941c79437 100644
--- a/.github/REVIEW_RULES.md
+++ b/.github/REVIEW_RULES.md
@@ -122,7 +122,7 @@ Return a single JSON object:
     "proves_the_claim": "proves_it" | "weaker_than_claimed" | "mismatch" | "unverifiable",
     "claim_note": "<one sentence: what the main theorem actually says, especially where it is narrower than the card's prose>",
     "assumed_inputs": "<what the headline takes as hypothesis rather than proving, and whether the card discloses it; empty if it assumes nothing>",
-    "already_formalized": "<Mathlib or pool declaration that already proves this, or empty>",
+    "already_formalized": "<the Mathlib or pool declaration that already proves this — a bare declaration name and nothing else. Leave EMPTY if you found none or could not check; do not write a sentence here, and never use it to say the question is unverifiable>",
     "source_match": "matches" | "mismatch" | "unverifiable" | "not_a_known_result",
     "code_quality": <int 1-5 where 1 = clear AI slop, 3 = competent, 5 = mathlib-merge-ready; anything other than 3 needs a finding or the note below to point at what earned it>,
     "significance_one_sentence": "<one sentence: what would a mathematician say the contribution is, or why it isn't one>"
diff --git a/python/lean_pool/review.py b/python/lean_pool/review.py
index 19e7f89306..f465d0c3ed 100644
--- a/python/lean_pool/review.py
+++ b/python/lean_pool/review.py
@@ -1179,7 +1179,7 @@ def render_project_assessment(payload: dict) -> str:
     ]
     already = (a.get("already_formalized") or "").strip()
     if already:
-        rows.append(("Already formalized", f"🛑 `{already}`"))
+        rows.append(("Already formalized", _prior_art_cell(already)))
     assumed = (a.get("assumed_inputs") or "").strip()
     if assumed:
         rows.append(("Assumed, not proved", assumed))
@@ -1266,7 +1266,7 @@ def render_challenge_assessment(payload: dict) -> str:
     ]
     already = (a.get("already_formalized") or "").strip()
     if already:
-        rows.append(("Already formalized", f"🛑 `{already}`"))
+        rows.append(("Already formalized", _prior_art_cell(already)))
 
     table = "| Aspect | Value |\n|---|---|\n"
     for key, value in rows:
@@ -1288,6 +1288,21 @@ def _icon_cell(icons: dict[str, str], value: str) -> str:
     return f"{icons.get(value, '•')} `{value}`"
 
 
+def _prior_art_cell(value: str) -> str:
+    """Render an ``already_formalized`` value at its actual confidence.
+
+    The field is specified as a declaration name or nothing, but the
+    model sometimes answers the question in prose instead — the first
+    production run under the new rules returned "unverifiable from the
+    supplied diff". Stamping 🛑 on that reads as "this is a duplicate" on
+    a PR the same review approved, which is the opposite of what it said.
+    Treat a multi-word answer as the hedge it is.
+    """
+    if " " in value:
+        return f"🟡 {value}"
+    return f"🛑 `{value}`"
+
+
 def render_solution_assessment(payload: dict) -> str:
     """Render a solution assessment block as a Markdown table."""
     a = payload.get("assessment") or {}
diff --git a/python/tests/test_review.py b/python/tests/test_review.py
index 417d66bccc..6ea10f2410 100644
--- a/python/tests/test_review.py
+++ b/python/tests/test_review.py
@@ -949,6 +949,27 @@ def test_project_assessment_leads_with_the_ungated_checks() -> None:
     assert "Obscure problem" not in table
 
 
+def test_prior_art_hedge_is_not_rendered_as_a_duplicate() -> None:
+    """A prose non-answer must not wear the stop icon a real hit earns.
+
+    The first production run under these rules answered
+    `already_formalized` with "unverifiable from the supplied diff" on a
+    PR it approved; rendering that with 🛑 said the opposite.
+    """
+    from lean_pool.review import render_project_assessment
+
+    hedged = render_project_assessment(
+        {"assessment": {"already_formalized": "unverifiable from the supplied diff"}}
+    )
+    hit = render_project_assessment(
+        {"assessment": {"already_formalized": "SimpleGraph.nonempty_hom"}}
+    )
+
+    assert "🛑" not in hedged
+    assert "🟡 unverifiable from the supplied diff" in hedged
+    assert "🛑 `SimpleGraph.nonempty_hom`" in hit
+
+
 def test_project_assessment_omits_empty_optional_rows() -> None:
     """A clean project shows no prior-art or assumption row at all."""
     from lean_pool.review import render_project_assessment