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": , "estimate_basis": "", - "already_formalized": "", + "already_formalized": "", "assessment_one_sentence": "" }, "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": "", "assumed_inputs": "", - "already_formalized": "", + "already_formalized": "", "source_match": "matches" | "mismatch" | "unverifiable" | "not_a_known_result", "code_quality": , "significance_one_sentence": "" 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