LLM review: check what the gates can't, and route non-content PRs away

[Vilin97]

Audits the review prompts against the pool as it actually is (141 projects), against all 148 reviews the bot has posted and what happened to those PRs afterwards, and against how Tau Ceti and ArkLib review contributions. Three things came out of it.

The project review never asked the question that decides these PRs

Every defect a human audit has caught in this repository lives in the gap between what a card claims and what its Lean proves — and nothing in REVIEW_RULES.md asked about it. statement-mismatch appears only as an example tag in the output schema, never as a check.

PR	LLM said	What was true
#275	approve, good_fit, 0 findings	closed — headline follows in a few lines from Mathlib's Finsubgraph
#225	one finding, on card wording	diagonal lemma postulated as an inductive constructor (invisible to #print axioms), and subsumed by the pool's own Incompleteness
#278	approve, 4/5, 0 findings on a 710k-token partial diff	closed — 92% machine-emitted certificates riding an internal Mathlib API
#215 / #240 / #265 / #199	approved as claimed	a rescaled surrogate tableau; a card informal that was false; a synthetic residue model presented as the geometry; NP-hardness claimed for a reduction-correctness result

So the project rules gain the four checks the challenge rules have always had, adapted for finished proofs: does the Lean prove what the card claims, what is assumed rather than proved, is it already done, and does the cited source support it. Plus a generated-bulk criterion and an AI-slop list — half the pool is AI-written, and fluent prose is not evidence.

Both comparison repos converge on this shape. Tau Ceti runs correctness and reuse first because they block most often per dollar, and tells reviewers not to "defer to fluent prose, confident docstrings, plausible-looking names"; ArkLib forbids a docstring from being the sole basis of a blocking correctness claim. Their bigger structural ideas — a reviewer with a checkout and grep, per-angle agents, deterministic verdicts — are noted below as follow-ups, not done here.

Infra PRs were being graded for mathematical fit

A .lean file under scripts/ clears the workflow's "touches Lean?" filter, and classify_pr then fell through to project. The exposition PRs landed on the fit rubric: #279 and #282 came back not_a_fit / undergraduate; #283, the next increment of the same pipeline, came back good_fit / graduate / approve over a summary that opened "This is not a mathematics contribution." All three merged. classify_pr now returns infra and posts a note instead of calling the model.

Calibration, from the same audit

• obscure_problem was no in 147 of 147 project reviews — removed.
• Card metadata moved to out-of-scope: 19 of 81 findings were card/anchor nits, and [import] RellichKondrachov #216 and Import bannai-bannai-stanton: bound on distance sets #243 were rejected on nothing else, then merged unchanged. quality.py already gates the schema.
• A partial review may no longer approve — code_quality cannot be scored on files the model never saw, which is exactly what happened on Import Erdos97ConvexOctagon: convex-octagon case of Erdős Problem 97 #278.
• The sticky comment now says request_changes is an ask, not a close: 39% of those verdicts were merged after a human looked, while 20 of 28 closures cited the bot.
• Two of the four approve-examples (sphere packing, Erdős 124) were not in the pool at all. Replaced with real slugs, plus the pool's real size distribution (median ~2,800 lines; only 4 of 138 under 500) and CS/physics examples, since ~a quarter of the pool is MSC 68/94/81/91 and the rules called it "formal-mathematics" throughout.

The reviewer can now read the PR description

REVIEW_RULES.md has always allowed the source anchor to live in the "PR description" — which was never sent to the model. It is now, along with the title.

Both are contributor-written, and so is the diff, so they are fenced with a per-request random token and framed as claims to verify rather than instructions. A static delimiter can be closed by the text it delimits; a fresh one cannot be guessed by whoever writes the PR. Every review mode also gets an explicit trust boundary, with prompt-injection as a finding tag.

Not done here

Worth discussing separately: giving the reviewer a checkout and grep so "is this already in Mathlib?" is answerable rather than guessed; splitting the monolithic prompt into per-angle agents; computing the verdict from the findings instead of asking for it; and an adversarial pass that tries to refute each finding. The refactor and solution rules have never once run in production (0 invocations each) — worth checking that routing separately.

Tested with 302 Python tests; new coverage for the routing fix, the fenced PR context, the trust boundary across all four modes, the reordered assessment table, and the request_changes footer.

🤖 Generated with Claude Code

[greptile-apps]

Greptile Summary

This PR makes three improvements to the LLM review pipeline: it adds four correctness-focused checks to the project review prompt (claim-vs-Lean mismatch, assumed inputs, duplication, source accuracy), fixes infra PRs being routed to the mathematical-fit rubric, and passes the PR title and description to the model as fenced, per-request-tokenised contributor evidence.

• Routing fix: classify_pr now returns "infra" (posting a skip note) when no .lean file is under LeanPool/, Challenge/, or Solution/, preventing exposition/CI PRs from being graded on mathematical fit; old behavior fell through to "project" for any Lean-touching PR.
• Prompt improvements: REVIEW_RULES.md adds checks 1–5 (proves-the-claim, assumed inputs, duplication, source match, AI-slop tells), retires the always-false obscure_problem field, replaces fictional calibration examples with real pool slugs, and clarifies that request_changes is an ask, not a close.
• PR context injection: fetch_pr_context retrieves the PR title and description via the GitHub API; both are rendered into the user message using a fresh secrets.token_hex(8) fence so contributor text cannot escape its boundary by containing the delimiter.

Confidence Score: 5/5

Safe to merge: routing logic is correct, all new code paths are tested, and the fencing approach for PR descriptions is sound.

The infra routing fix only activates after all existing challenge/solution/refactor checks have returned, leaving those paths unchanged. touches_reviewable_content correctly mirrors what classify_pr already tracks without duplicating the early-return logic. The fence token is generated fresh per request with 64 bits of entropy, so it cannot be pre-committed in a PR description. New tests cover all changed code paths including edge cases (empty description, null body, large body truncation, every review mode).

Files Needing Attention: No files require special attention.

Important Files Changed

Filename	Overview
python/lean_pool/review.py	Adds touches_reviewable_content, PullRequestContext, fetch_pr_context, render_pr_context, and render_infra_skip_comment; updates classify_pr, build_user_content, request_review, and render_project_assessment. Logic is correct: refactor/challenge/solution early returns precede the new infra check, and touches_reviewable_content correctly excludes generated root indices.
.github/REVIEW_RULES.md	Adds structured checks 1–5, updates calibration examples to real pool slugs, removes obscure_problem, adds not_applicable fit value, and clarifies the partial-review rule. Output schema and narrative are consistent with the Python rendering changes.
python/tests/test_review.py	New tests cover infra routing, touches_reviewable_content edge cases, trust-boundary presence across all review modes, PR context inclusion and truncation, round-trip Markdown fidelity, assessment table ordering, the request_changes footer, and the infra skip comment.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
    A[classify_pr called] --> B{new challenge added?}
    B -- yes --> C[return 'challenge']
    B -- no --> D{solution file touched?}
    D -- yes --> E[return 'solution']
    D -- no --> F{challenge modified without pool content?}
    F -- yes --> G[return 'challenge']
    F -- no --> H{only existing projects, no new?}
    H -- yes --> I[return 'refactor']
    H -- no --> J{touches_reviewable_content?}
    J -- no --> K[return 'infra — post skip note']
    J -- yes --> L[return 'project']

    style K fill:#ffcccc,stroke:#cc0000
    style L fill:#ccffcc,stroke:#00aa00

Loading

_{Reviews (3): Last reviewed commit: "Lead the assessment table with the ungat..." | Re-trigger Greptile}

[Vilin97]

Fixed the stale classify_pr docstring in 1bb0787 — thanks, that sentence still promised the "project" fallback the function no longer takes.

[Vilin97]

Acted on the row-ordering note too (b478385). The docstring already said fit and level should sit below the ungated checks, but the code still had Fit in the top row — directly beneath the verdict line it echoes. Fit/Level/Branch/Mode now follow the claim, source, prior-art, and assumption rows, and the list is built in display order instead of inserting at index 3.