Search Mathlib and the pool before asking whether a PR is new

[Vilin97]

Closes the one gap the audit left open. REVIEW_RULES.md asks whether a headline is already proved; the reviewer had no way to find out. Its first production run under the new rules answered already_formalized with "unverifiable from the supplied diff" — honest, and useless.

That question has already cost two merges: #275 was approved with zero findings and closed by hand for duplicating SimpleGraph.nonempty_hom_of_forall_finite_subgraph_hom, and #225 was closed as subsumed by the pool's own Incompleteness.

It finds the real duplicate, and doesn't invent one

I put both PRs' actual headlines through the live index before building anything:

Query	Top hits
#275: "every graph is k-colorable if every finite subgraph is"	SimpleGraph.Colorable, SimpleGraph.chromaticNumber, … SimpleGraph.nonempty_hom_of_forall_finite_subgraph_hom — "The De Bruijn–Erdős Theorem for Graph Homomorphisms" (5th of 6)
#285: "distinct subset sums, 4^n − 1 bound on sum of squares"	Set.Finite.induction_on_subset, Nat.sum_four_squares, UniqueSums — nothing relevant

The miss is recoverable and a genuinely new result stays clean, so an empty result is usable as evidence of novelty rather than a shrug. Note the real hit ranked fifth — hence six hits per claim, not one.

What gets searched

• Mathlib, via LeanExplore's hybrid name-and-meaning search, on the (declaration, informal) pairs already in the card — precise, and typically 1–5 queries per PR.
• The pool, as all 141 projects in slug: title [tags] form, ~4k tokens. No similarity heuristic beats handing over the complete list, and Import godel-loeb formalization #225 shows pooled prior art counts the same as Mathlib's.

Design notes

Pre-computed, not a tool call. Deterministic, unit-testable, one round trip whether or not the model would have thought to look. It also sidesteps the reported reasoning_effort + function-tools incompatibility on gpt-5.6-sol, which would have forced a choice between searching and xhigh.

Scoped. Only project and challenge PRs, and only headlines the PR adds — a refactor or a bump would otherwise re-litigate prior art settled when the thing it touches merged.

Trust. These are our results, so they sit outside the contributor fence from #293 — but the section and check 3 both say a hit is a candidate, that shared vocabulary is not duplication, and that the declaration must be read before anything is called a duplicate.

Never fatal. Missing key, backend down, or malformed YAML each degrade to a stated "not searched", which the rules distinguish from a clean miss so silence is never mistaken for absence of prior art. LEANEXPLORE_API_KEY was already a repo secret; it's now passed to the review step.

Check 3 is rewritten to use the evidence: if the search ran and found nothing, say so and leave already_formalized empty; unverifiable is only for a search that could not run, and belongs in the prose rather than in a field that holds a declaration name.

Verified the lean-explore API against the installed package rather than assuming — SearchResult has no description field, so the prose comes from informalization with docstring as fallback. 316 tests, including a regression test built from the #275 case.

🤖 Generated with Claude Code

[greptile-apps]

Greptile Summary

This PR introduces pre-computed Mathlib and pool prior-art search for project and challenge PRs, closing the gap where the LLM reviewer had no way to answer the "is it already done?" check in REVIEW_RULES.md. Both previously flagged issues in this PR (the --jq/raw-Accept incompatibility in fetch_file_at and per-claim failures silently rendering as "no match found") are resolved in the current head.

• python/lean_pool/prior_art.py (new module): extracts new claims from registry diffs, runs async LeanExplore queries per headline, maps each per-claim exception to None (distinct from an empty hit list), and renders a Prior art section that clearly distinguishes a clean miss from a failed or skipped search.
• python/lean_pool/review.py: adds fetch_file_at (raw Accept header, no --jq) and gather_prior_art, which are wired into request_review as a pre-computed prior_art_section passed outside the untrusted contributor fence.
• .github/workflows/llm-review.yml: injects LEANEXPLORE_API_KEY into the review step; the feature would silently degrade without this even if the secret existed.

Confidence Score: 5/5

Safe to merge. The new prior-art path degrades gracefully at every failure point — missing key, backend error, unreadable registry, or per-claim timeout each produce a clearly-labelled 'not searched' note rather than a crash or a false clean-miss.

Both previously flagged defects are fixed in this head: fetch_file_at no longer pairs the raw Accept header with --jq, and per-claim async failures map to None in the hits dict rather than being dropped. The render function distinguishes None (search errored) from [] (search ran, nothing found) from absent key entirely. The 316-test suite, including regression coverage for the #275 duplicate case and the unreadable-registry edge case, exercises every meaningful failure mode.

Files Needing Attention: No files require special attention.

Important Files Changed

Filename	Overview
python/lean_pool/prior_art.py	New module implementing pre-computed Mathlib + pool prior-art search; correctly maps per-claim async failures to None (distinct from an empty hit list), degrades gracefully on missing API key or backend failure, and renders search results as candidates not verdicts.
python/lean_pool/review.py	Adds fetch_file_at (using raw Accept header, no --jq) and gather_prior_art; wires the prior-art section into request_review; both previously flagged issues (incompatible gh-API flags, per-claim failures masking as novelty) are resolved in this head.
.github/workflows/llm-review.yml	Adds LEANEXPLORE_API_KEY env-var injection to the review step; without this the secret would never reach search_mathlib even if set as a repo secret.
python/tests/test_prior_art.py	Comprehensive tests covering new-claims scoping, per-claim failure mapping to None, clean-miss vs. failure distinction, unreadable registry, and the #275 regression case; all important failure modes are exercised.
python/tests/conftest.py	Adds a lean_explore stub alongside the existing openai stub; uses setdefault so developers with the review group installed exercise the real package, while CI without it uses the stub.
.github/REVIEW_RULES.md	Check 3 rewritten to use the now-supplied Prior Art section; unverifiable is reserved for searches that could not run, and hits are explicitly framed as candidates not verdicts.
python/pyproject.toml	Adds lean-explore>=0.4 to the review dependency group; lock resolves to 1.2.1.
python/tests/test_review.py	Existing test suite unchanged structurally; prior-art integration tests for gather_prior_art / fetch_file_at are covered in test_prior_art.py.

Sequence Diagram

sequenceDiagram
    participant W as Workflow (llm-review.yml)
    participant M as main()
    participant G as gather_prior_art()
    participant F as fetch_file_at()
    participant GH as GitHub API
    participant S as search_mathlib()
    participant LE as LeanExplore API
    participant R as render()
    participant LLM as OpenAI Model

    W->>M: uv run python -m lean_pool.review
    M->>M: classify_pr() → kind
    Note over M: kind in {project, challenge, refactor, solution, infra}
    M->>G: gather_prior_art(kind, head_sha, repo)
    alt kind not in (project, challenge)
        G-->>M: None
    else
        G->>F: fetch_file_at(registry, head_sha)
        F->>GH: "GET repos/{repo}/contents/{registry}?ref={sha} Accept: raw+json"
        GH-->>F: raw YAML bytes
        F-->>G: head_text (or empty string on error)
        G->>G: read base_text from disk (checked-out base branch)
        G->>G: new_claims(head_text, base_text, kind)
        G->>S: search_mathlib(claims)
        alt LEANEXPLORE_API_KEY not set
            S-->>G: "({}, reason)"
        else per-claim async search
            S->>LE: asyncio.gather([client.search(claim.query) ...])
            LE-->>S: hits per claim (or exception mapped to None)
            S-->>G: (hits_by_declaration, None)
        end
        G->>G: read projects.yml for pool index
        G->>R: render(claims, hits, projects_text, unavailable)
        R-->>G: prior_art_section (Markdown)
        G-->>M: prior_art_section
    end
    M->>LLM: request_review(rules, diff, prior_art_section, ...)
    LLM-->>M: structured JSON verdict
    M->>GH: post_comment(render_comment(...))

Loading

_{Reviews (4): Last reviewed commit: "Stub lean_explore for the test environme..." | Re-trigger Greptile}

[github-actions]

LLM review skipped: PR touches no .lean files. Push a Lean change or comment /review after one lands to re-trigger.

[Vilin97]

Verified and fixed — that was a real, total failure of the feature, not a lint nit.

gh api ... --jq ".content" --header "Accept: application/vnd.github.raw+json" exits 1 with invalid character 'p' looking for beginning of value: the raw media type returns file bytes, so there is no JSON for jq to filter. That non-zero exit was caught and turned into "", which new_claims read as an empty registry — every prior-art section would have reported "this PR adds no new headline" and no Mathlib search would ever have run.

My own dry run missed it because it fabricated the head registry instead of fetching one. Against PR #285's real head the fixed call returns 248,015 characters and three headlines.

Added two guards so it cannot fail silently again: gather_prior_art now distinguishes an unreadable registry from a PR that genuinely adds nothing (both yield zero claims; only one means prior art went unchecked), and a test pins the gh argument shape, since the broken and working forms differ by one flag.

[github-actions]

LLM review skipped: PR touches no .lean files. Push a Lean change or comment /review after one lands to re-trigger.

[Vilin97]

Fixed in 8faf8f5 — verified, and it's the same bug class as the fetch one, a level down.

asyncio.gather(return_exceptions=True) returns exceptions inline, and _search_all filtered them out with if not isinstance(hits, BaseException). A headline whose query timed out therefore vanished from the mapping, hits.get(decl) returned None, and render fell through to "No Mathlib declaration matched this statement" — one flaky query reported as evidence of novelty.

A failed claim now maps to None and renders as "This headline's search failed; prior art for it is unchecked." Two tests: one on the gather seam (one query raises, both keys survive, the failed one is None), one on what the rendered section says for each of the three outcomes — hit, clean miss, failed query.

[github-actions]

LLM review skipped: PR touches no .lean files. Push a Lean change or comment /review after one lands to re-trigger.

[github-actions]

LLM review skipped: PR touches no .lean files. Push a Lean change or comment /review after one lands to re-trigger.