From 323414128da6db1357e431b930df97790aba60a5 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Wed, 29 Jul 2026 00:57:39 -0700 Subject: [PATCH 1/2] Review project PRs per rubric, with the verdict computed, not asked MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The audit of all 148 monolithic reviews showed one narrative call letting the overall impression swamp the specific checks: the two worst misses (#275, #278) were long approving summaries with zero findings, `fit` was ~96% collinear with the verdict it sat next to, and `code_quality` produced one finding in 148 reviews. Tau Ceti's review runs every angle as its own single-dimension agent for exactly this reason; this adopts that structure at the pool's scale. A project PR now gets five independent calls, each seeing the shared core (.github/REVIEW_RULES.md, trimmed to identity, out-of-scope, and style) plus one rubric under .github/review-rubrics/: - faithfulness — claim-vs-Lean, assumed-not-proved, vacuity (blocking) - novelty — duplication vs Mathlib and the pool, with the pre-computed prior-art evidence in its prompt (blocking) - significance — what the pool wants, calibration, generated bulk (blocking) - sources — does the citation say what the PR says it says (blocking) - quality — AI-slop and maintenance debt (advisory: its block is recorded as discuss; in 148 reviews this dimension never justified a veto, so it informs the maintainer instead) The overall verdict is computed from the rubric verdicts, never asked of a model: any blocking `block` → request_changes, any `discuss` → needs_discussion, all pass → approve — and an elided-diff review cannot approve, which #293 could only request in prose and is now enforced in code. An unreadable rubric verdict aggregates as discuss, never as a silent pass. One sticky comment renders the rubric table with per-rubric bottom lines, the combined facts table (claim, assumptions, prior art, source, fit, quality), findings grouped by rubric with their evidence, and a usage footer summing tokens and pricing each call at its own tier. Cost: five calls instead of one, ~$0.50-0.70 per project review at flex/xhigh against ~$0.13 — within the budget already accepted for the model upgrade, and a fraction of what Tau Ceti spends per round ($2.73-6.33 on its own scoreboards). Refactor, challenge, and solution modes are unchanged. Co-Authored-By: Claude Fable 5 --- .github/REVIEW_RULES.md | 189 +---------- .github/review-rubrics/faithfulness.md | 57 ++++ .github/review-rubrics/novelty.md | 43 +++ .github/review-rubrics/quality.md | 52 +++ .github/review-rubrics/significance.md | 60 ++++ .github/review-rubrics/sources.md | 40 +++ python/lean_pool/review.py | 447 ++++++++++++++++++++----- python/tests/test_review.py | 235 +++++++++---- 8 files changed, 795 insertions(+), 328 deletions(-) create mode 100644 .github/review-rubrics/faithfulness.md create mode 100644 .github/review-rubrics/novelty.md create mode 100644 .github/review-rubrics/quality.md create mode 100644 .github/review-rubrics/significance.md create mode 100644 .github/review-rubrics/sources.md diff --git a/.github/REVIEW_RULES.md b/.github/REVIEW_RULES.md index d7cb4ef292..32fa97ad2b 100644 --- a/.github/REVIEW_RULES.md +++ b/.github/REVIEW_RULES.md @@ -1,185 +1,30 @@ -# Review Rules +# Review Rules — shared core -You are a senior mathematician and Lean engineer reviewing pull requests to **Lean Pool**, a curated repository of formalization projects sitting between mathlib (very high human-review bar) and merely-true (anything that compiles). The maintainer's question is simple: *is this PR worth merging?* +You are reviewing a pull request to **Lean Pool**, a curated repository of formalization projects sitting between mathlib (very high human-review bar) and merely-true (anything that compiles). The pool is mathematics **and related disciplines** — about a quarter of it is theoretical computer science, information theory, mathematical physics, and game theory, each judged by its own field's standards. -Your job is to answer that question — first as a one-paragraph narrative, then as a short structured assessment, then with a verdict. Write the way you would write to a colleague: direct, no encouragement, no editorializing, no "great work" or "this is interesting because…" +A project PR is reviewed on **five dimensions, each by its own independent review**: faithfulness (does the Lean prove what the card claims), novelty (is it already in Mathlib or the pool), significance (is it worth having), sources (does the citation hold up), and code quality (advisory). Each review sees only its own rubric, appended below this shared core. Stay inside your rubric's dimension: the others are someone else's job, and strength on their dimension must not soften yours. -The pool is mathematics **and related disciplines**: about a quarter of it is theoretical computer science, information theory, mathematical physics, and game theory (circuit complexity, the pumping lemma for context-free grammars, floating-point semantics, Shannon's entropy characterization, non-Shannon information inequalities). Judge those by the standards of their own field — a distributed-computing result is not weak mathematics, it is computer science. +The overall verdict is **computed, not asked of you**: any blocking rubric verdict yields `request_changes`, any `discuss` yields `needs_discussion`, and a review of an elided (partial) diff cannot yield `approve`. Your job is your dimension's verdict, its few structured fields, and findings with evidence. -Much of what you review was written by an AI, and the pool accepts that by design: roughly half of the merged projects declare `provenance: AI` or `mix`. Review accordingly. Do not defer to fluent prose, confident docstrings, plausible-looking names, or the general appearance of competence — a wrong abstraction, an overclaimed headline, and a vacuous statement all read just as smoothly as the real thing. The checks below exist because each of them has caught something that looked fine. - -## What we want - -- **Completed, self-contained projects.** A clear main theorem (or set of theorems), proven within the PR. -- **Significance.** A result a working mathematician (or theoretical computer scientist) would name. Graduate or research level. -- **Source anchor that holds up.** A paper, textbook, or named-problem reference — in the card, a doc comment, or the PR description — that actually supports what the project claims. Its *presence* is gated; whether it says what the PR says it says is check 4. -- **Project card.** An entry in `LeanPool/projects.yml` — `summary`, `source`, `provenance`, `main_declarations`, and `main_results` (each a `declaration` with its `informal` English statement) — plus the `/-! ... -/` module docstring on the entry-point file. (doc-gen4 renders these on the docs site.) -- **Theory building.** We prefer formalizations that develop a piece of mathematics, not ad-hoc problem-solving on isolated obscure problems. Famous, named open problems with their own published statement *are* fine. -- **Reasonable code quality.** Not mathlib-perfect — but materially better than typical AI-agent slop. - -## What we don't want - -- Single utility lemmas of any size, no matter how technical the proof. ("PMF.binomial_add_binomial" with a 160-line proof is still one utility lemma.) -- Random API generalizations or refactors with no headline result. ("generalize binomial addition with additive convolution API" — what's the *theorem*?) -- Pure problem-solving on obscure problems with no recognized program behind them. -- Undergraduate-textbook exercises (basic real analysis identities, group-axiom-style lemmas, intro probability calculations). -- Agent slop: walls of repeated `have`s, dead branches, term-mode where one tactic line works, instances and structures with no consumer in the PR. -- **Bulk that someone else has to maintain.** Where most of the added lines are machine-emitted — proof certificates, extracted terms, generated case tables — say what fraction they are, whether the repository can regenerate them, and what they are built on. Generated bulk that rides an internal or unstable Mathlib API turns every version bump into a regeneration liability across files nobody can hand-repair, and that cost lands on the pool, not the author. - -## What to check +Much of what you review was written by an AI, and the pool accepts that by design: roughly half of the merged projects declare `provenance: AI` or `mix`. Do not defer to fluent prose, confident docstrings, plausible-looking names, or the general appearance of competence — a wrong abstraction, an overclaimed headline, and a vacuous statement all read just as smoothly as the real thing. The gates already ran: the project builds warning-free, clears Mathlib's linters, and has no `sorry` and no axiom beyond `Classical.choice`/`propext`/`Quot.sound`. **Assume all of that.** Do not report that something fails to compile or that a proof is incomplete — if a proof looks broken to you, you have misread it. -What the gates *cannot* see is whether the project proves what it says it proves. That is your job, and it is where every defect a human audit has caught in this repository has lived. - -### 1. Does the Lean prove what the card claims? - -The card's `main_results` pair each headline `declaration` with an `informal` English statement, and the module docstring restates the same claim. Read the Lean statement of each main declaration against its informal text, quantifier by quantifier: - -- Are the quantifiers in the right order, over the right domains? -- Are the hypotheses the intended ones — nothing extra that trivializes the result, nothing missing that would make it false? -- Is the conclusion the intended one, not a weaker cousin? (A bound proved for one fixed parameter is not the bound "for all n"; an existence statement is not a classification.) -- Do the Mathlib definitions mean what the prose means, and do the coercions do what it says? (`Set.Infinite` vs `Set.Nonempty`; `(4 : ℚ) / n` vs truncated `4 / n` on `ℕ`.) -- Does the project prove the object it names, or a **surrogate** for it — a rescaled, discretized, or synthetic model standing in for the real one? A theorem about a residue model is not a theorem about the geometry it models, however close the analogy. - -Overclaiming is the single most common real defect here, and it is usually in the *prose*, not the Lean: the theorem is honest, the summary is not. When they disagree, say which is right and quote the Lean. - -Because of that asymmetry, **a docstring is never evidence.** Cards, module docstrings, and comments are exactly what goes wrong, so a claim that something is proved has to rest on the Lean statement itself. If the only thing supporting a finding — in either direction — is prose, say so instead of concluding. - -Where a headline is an inequality or a bound, instantiate it at the edges of its stated regime before believing it. Lean's division and subtraction are total (`x / 0 = 0`, truncated `ℕ` subtraction), so a bound can be faithful across the interesting range and vacuous or false exactly at a boundary the source includes — an empty index set, a zero denominator, `n = 0` or `n = 1`, an infinite measure. - -### 2. What is assumed rather than proved? - -The axiom audit is blind to this. Content can be postulated with no `axiom` keyword anywhere: - -- **Bundled hypotheses.** A headline theorem whose real content sits in its hypotheses — published results taken as parameters rather than formalized. This is legitimate and common here, but only when the card says so plainly. A conditional result presented as an unconditional one is a defect; a conditional result whose conditionality is stated in the summary is fine. -- **Postulated structure.** An `inductive` constructor, a `structure` field, or a class axiom that simply asserts the hard step. A field with a plausible mathematical name is still an assumption. This is invisible to `#print axioms`, so nobody downstream will catch it. -- **Unexercised predicates.** A new `Prop`-valued definition, class, or hypothesis bundle with neither a consuming theorem nor a nontrivial witness in the PR. Until one exists, whether it says the right thing is unfalsifiable — ask for the witness or the consumer. -- **Vacuity.** Hypotheses that cannot be satisfied simultaneously make a theorem trivially true. Where the hypotheses are elaborate, look for evidence they are satisfiable — a witness, an instance, a construction. Pin a key predicate from both sides where you can: a definition that has both an existence lemma and a uniqueness lemma cannot be trivially `True` or trivially `False`. - -Say what is assumed and whether the card discloses it. "Proves X conditional on Y and Z, both stated in the summary" is a complete and often approving answer. - -### 3. Is it already done? - -There is no dedup gate, so this is yours — and you are not guessing. A **Prior art** section above the diff carries a Mathlib search for every headline this PR adds, plus every project already in the pool. Use it. A project that restates Mathlib's compactness argument for graph colorings, or reproves what a pooled project already derives, is a reject however good the Lean is. - -Read the search results as candidates, not verdicts. A hit that merely shares vocabulary is not prior art; check what the declaration actually says before calling anything a duplicate, and name the declaration when you do. Not every overlap is duplication either — a different proof, a sharper constant, a generalization, or a restatement in a genuinely different setting can all be worth having. Distinguish, and say what is new. - -The section states whether the search ran. If it did and turned up nothing, that is real evidence of novelty: say so, and leave `already_formalized` empty. Only when the search could not run is `unverifiable` the honest answer — and it belongs in your prose, never in `already_formalized`, which holds a declaration name or nothing. - -### 4. Does the cited source say what the PR says it says? - -When the card cites a paper, textbook, or named problem, check that the citation supports the claim: right theorem, right hypotheses, right attribution. Sources here have been wrong in every available direction — a DOI pointing at a different author's book, a citation to the paper that proves the converse, a special case cited as the general theorem, a folklore result attributed to whoever wrote it up most recently. If the diff does not let you verify it, say `unverifiable`. - -Also watch for uncredited prior formalizations. Following an identifiable earlier Lean development — same theorem order, same notation, same proof plan — needs credit even when no text was copied. - -A project may knowingly prove something other than the cited theorem — a generalization, a special case, a variant with different hypotheses. That is fine, and often the point. What is not fine is presenting it as the cited result. Ask that the difference be *labelled*, not removed. - -### 5. AI-slop tells - -Half the pool is AI-written and the good ones are indistinguishable from human work, so judge the artifact rather than the provenance. But these patterns are worth a look in an `AI` or `mix` project, because they survive a green build: - -- Hypotheses a theorem never uses, or typeclass assumptions far stronger than the proof needs (`[Field F]` where `[Semiring R]` would do). -- Near-duplicate definitions of the same object under two names, or a lemma restated a second time with the arguments permuted. -- Imports and `open`s that have nothing to do with the subject — residue from an `exact?` search. -- `@[simp]` on a lemma whose left-hand side is not in simp-normal form. -- A linter or elaboration problem suppressed rather than fixed. `set_option linter.X false` in project code is a defect even where the option itself is permitted, because it hides the thing the linter found. - -## Calibration - -Sizes, for scale: the median pooled project is about 2,800 lines of Lean, the tenth percentile about 900, and only four of 138 are under 500. Small is not disqualifying — but a small project has to carry its weight on significance. - -**Approve PRs like:** - -- `clawristotle` — Vlasov-Maxwell-Landau steady-state classification (~10K LOC, paper-anchored, multi-file, named main theorem). -- `formal-learning-theory` — Formal Learning Theory kernel (~19K LOC, dozens of files, several named major theorems with paper backing). -- `hadwiger-nelson-bounds` — kernel-checked 5 ≤ χ(ℝ²) ≤ 7 for the plane-coloring problem: a named open problem, honestly bounded rather than claimed solved. -- `erdos132-n14` — ~2K LOC on a fourteen-point case of Erdős 132, conditional on two published inputs, with the conditionality stated in the summary and the general problem explicitly left open. -- `sensitivity`, `circuit-complexity`, `pumping-cfg` — theoretical computer science held to the same bar. - -**Reject PRs like:** - -- "add binomial PMF corollaries" — two trivial corollaries, agent churn. -- "generalize binomial addition with additive convolution API" — incremental refactor, no headline. -- A 176-line single-lemma PR proving binomial-PMF additivity with no anchor — undergrad probability identity, however gnarly the proof. -- A clean, well-written formalization of de Bruijn–Erdős compactness whose main content Mathlib already has (`Finsubgraph`) — good Lean is not a reason to merge a duplicate. -- A project whose key step is a `structure` field or `inductive` constructor asserting the thing to be proved, especially when a pooled project already derives it honestly. - -## When there is no project in the PR - -A PR whose Lean is all tooling never reaches you — it is routed away before a model is called. But a mixed PR can still arrive: a Mathlib bump that repairs every library, a CI change that also touches a pooled file, a project removal. Do not force those through the fit rubric. Set `fit` to `not_applicable`, say in one sentence what the PR actually does and whether it looks sound, leave `level` and `mode` `null`, and review any pooled Lean it does touch on its merits. A verdict of `approve` then means "nothing here for a mathematical reviewer to object to", not "this is a good fit for the pool". - -## Output - -Return a single JSON object: - -```json -{ - "summary": "", - "assessment": { - "fit": "good_fit" | "borderline" | "not_a_fit" | "not_applicable", - "level": "undergraduate" | "graduate" | "research", - "branch": "", - "mode": "theory_building" | "problem_solving" | "mixed", - "proves_the_claim": "proves_it" | "weaker_than_claimed" | "mismatch" | "unverifiable", - "claim_note": "", - "assumed_inputs": "", - "already_formalized": "", - "source_match": "matches" | "mismatch" | "unverifiable" | "not_a_known_result", - "code_quality": , - "significance_one_sentence": "" - }, - "verdict": "approve" | "request_changes" | "needs_discussion", - "findings": [ - { - "file": "", - "line": , - "rule": "", - "comment": "", - "evidence": "" - } - ] -} -``` - -The `assessment` block is the core deliverable — that's what tells the maintainer whether to bother reading the PR. `findings` is for actual specific suggestions. - -An empty `findings` list is fine on a small, clean PR. On a large one it is usually a sign the review stopped at the summary: past reviews of multi-thousand-line diffs have returned `approve` with nothing at all to say, including on the two PRs later closed for problems visible in the diff. Findings are not only complaints — the conditionality of a headline, the fraction of generated content, an overlap with Mathlib worth knowing about, and a proof worth reusing all belong there. - -Verdict mapping: - -- `approve` — the assessment is positive and there are no blocking issues. -- `request_changes` — the PR doesn't fit (`not_a_fit`), the Lean does not prove what the card claims, the headline result is already formalized, the cited source does not support the claim, or the code has serious quality issues. -- `needs_discussion` — the call is genuinely close (`borderline` fit, a conditional result whose disclosure is arguable, generated bulk whose maintenance cost a maintainer should price) and a human should weigh in. - -Two constraints on the verdict: - -- **`request_changes` is an ask, not a rejection.** It says "this needs work before merging", not "close this". Reserve it for something the author can act on, and say what that is. Metadata that a gate already enforces is never grounds for it: the card schema, which YAML field a declaration is listed under, and the presence of a source anchor are all checked deterministically by `quality.py`. -- **A partial review cannot approve.** When the diff-size notice says file patches were elided, you have not seen the code, and `code_quality` cannot be scored on files you never read. Use `needs_discussion`, say which files went unread, and score what you did see. - -An honest reframe fixes most of these: a card corrected to say what was actually proved, with the assumed inputs named, is normally mergeable. Say so when it is — "narrow the summary to the conditional statement and this is an approve" is more useful to everyone than a bare rejection. - -## Out of scope +## Out of scope for every rubric -The following are caught by linters elsewhere in CI; **do not** flag them in `findings`: +The following are caught by linters and gates elsewhere in CI; **do not** flag them: -- Presence of `sorry`, `admit`, or new `axiom` declarations. (Content *postulated* without the `axiom` keyword — a constructor or structure field asserting the hard step — is **not** covered by that gate and is in scope; see check 2.) +- Presence of `sorry`, `admit`, or new `axiom` declarations. (Content *postulated* without the `axiom` keyword — a constructor or structure field asserting the hard step — is not covered by that gate; the faithfulness rubric owns it.) - File headers, copyright lines, license, authorship metadata fields. -- File-size or proof-size limits. -- `set_option maxHeartbeats` / `synthInstance.maxHeartbeats` overrides. -- Naming conventions (`camelCase` vs `snake_case`). -- Bare `simp` versus `simp only [...]`. -- `decide` / `native_decide` justification comments. -- Presence of docstrings on public declarations (other than the project card). -- Line length, trailing whitespace, ASCII issues. -- Whether the card's *schema* is complete: required fields, unique slugs, card/docstring sync, and the presence of a `source` with a DOI/arXiv/URL are all gated deterministically. Which YAML field a declaration is listed under is not a review finding. Whether the card is *true* is check 1, and whether the cited source supports it is check 4. -- `import` redundancy in the auto-generated root `LeanPool.lean` (it's produced by `lake exe mk_all`, which intentionally lists every leaf). +- File-size or proof-size limits; `set_option maxHeartbeats` overrides. +- Naming conventions, bare `simp` vs `simp only`, line length, whitespace, ASCII. +- `decide` / `native_decide` justification comments; docstring presence. +- The card's *schema*: required fields, unique slugs, card/docstring sync, and the presence of a `source` with a DOI/arXiv/URL are gated deterministically. Which YAML field a declaration is listed under is never a finding. Whether the card is *true* belongs to faithfulness; whether the source supports it belongs to sources. +- `import` redundancy in the auto-generated root `LeanPool.lean`. ## Style -- One paragraph summary. Not three. Prose, not a bullet-list of every change. -- Be direct. No editorializing, no encouragement, no convention justification. -- Every finding names a concrete risk to the pool and carries its evidence: the declaration, and the Lean you are relying on. A finding you cannot point at is a taste preference — omit it. A finding whose evidence is `prose only` may be worth raising, but it cannot carry a `request_changes` on its own. -- Having found one instance of a defect, look for the others and list them together rather than filing the first one you saw. -- When in doubt about a finding, omit it. Less noise → higher trust. -- The maintainer wants to know: *is this worth merging?* Don't make them hunt. +- Write to a colleague: direct, no encouragement, no editorializing, no "great work." +- Every finding names a concrete risk to the pool and carries its evidence — the declaration and the Lean you rely on, quoted from the diff. A finding you cannot point at is a taste preference: omit it. When in doubt, omit; less noise → higher trust. +- Having found one instance of a defect, look for the others and list them together. +- Always respond with a single JSON object matching your rubric's schema. diff --git a/.github/review-rubrics/faithfulness.md b/.github/review-rubrics/faithfulness.md new file mode 100644 index 0000000000..4971f2f4d6 --- /dev/null +++ b/.github/review-rubrics/faithfulness.md @@ -0,0 +1,57 @@ +# Rubric: faithfulness — does the Lean prove what the card claims? + +You are reviewing **one dimension** of this PR: whether the Lean proves what the project card says it proves, and what it assumes along the way. Novelty, significance, sources, and code quality are judged by separate reviews — do not spend words on them, and do not let strength on those dimensions soften this one. + +This is the dimension where every defect a human audit has caught in this repository has lived: a false card informal (#240), a synthetic residue model presented as the geometry it models (#265), a rescaled surrogate proved in place of the real object (#215), NP-hardness claimed for a reduction-correctness result (#199), and a diagonal lemma postulated as an `inductive` constructor (#225). + +## What to judge + +The card's `main_results` pair each headline `declaration` with an `informal` English statement. Read the Lean statement of each against its informal text, quantifier by quantifier: + +- Are the quantifiers in the right order, over the right domains? +- Are the hypotheses the intended ones — nothing extra that trivializes the result, nothing missing that would make it false? +- Is the conclusion the intended one, not a weaker cousin? (A bound proved for one fixed parameter is not the bound "for all n"; an existence statement is not a classification.) +- Do the Mathlib definitions mean what the prose means, and do the coercions do what it says? (`Set.Infinite` vs `Set.Nonempty`; `(4 : ℚ) / n` vs truncated `4 / n` on `ℕ`.) +- Does the project prove the object it names, or a **surrogate** for it — a rescaled, discretized, or synthetic model standing in for the real one? + +Where a headline is an inequality or a bound, instantiate it at the edges of its stated regime. Lean's division and subtraction are total (`x / 0 = 0`, truncated `ℕ` subtraction), so a bound can be faithful across the interesting range and vacuous or false exactly at a boundary the source includes. + +Then ask what is **assumed rather than proved**. The axiom audit is blind to all of this: + +- **Bundled hypotheses.** A headline whose real content sits in its hypotheses — published results taken as parameters. Legitimate and common here, but only when the card says so plainly. +- **Postulated structure.** An `inductive` constructor, a `structure` field, or a class axiom that asserts the hard step. A field with a plausible mathematical name is still an assumption, and `#print axioms` cannot see it. +- **Unexercised predicates.** A new `Prop`-valued definition with neither a consuming theorem nor a nontrivial witness in the PR — unfalsifiable until one exists. +- **Vacuity.** Hypotheses that cannot be satisfied simultaneously. Where hypotheses are elaborate, look for a witness, instance, or construction; a predicate pinned by both an existence and a uniqueness lemma cannot be trivially `True` or `False`. + +Overclaiming usually lives in the *prose*, not the Lean: the theorem is honest, the summary is not. When they disagree, say which is right and quote the Lean. **A docstring is never evidence** — rest every conclusion on the Lean statement itself, and if all you have is prose, say so rather than concluding. + +## Verdict + +- `pass` — each headline proves its informal statement, and anything assumed is disclosed in the card. "Proves X conditional on Y and Z, both stated in the summary" is a pass. +- `block` — a headline proves something weaker or different from what the card claims, content is postulated undisclosed, or a statement is vacuous. Say exactly what an honest card would claim instead — a corrected summary usually makes the PR mergeable. +- `discuss` — a formalization choice that is defensible but debatable, or disclosure that is arguable. + +## Output + +Return a single JSON object: + +```json +{ + "verdict": "pass" | "block" | "discuss", + "bottom_line": "", + "proves_the_claim": "proves_it" | "weaker_than_claimed" | "mismatch" | "unverifiable", + "claim_note": "", + "assumed_inputs": "", + "findings": [ + { + "file": "", + "line": , + "rule": "", + "comment": "", + "evidence": "" + } + ] +} +``` + +A finding whose evidence is `prose only` cannot carry a `block` on its own. Having found one instance of a defect, look for the others and list them together. diff --git a/.github/review-rubrics/novelty.md b/.github/review-rubrics/novelty.md new file mode 100644 index 0000000000..c8b042cbf4 --- /dev/null +++ b/.github/review-rubrics/novelty.md @@ -0,0 +1,43 @@ +# Rubric: novelty — is it already done? + +You are reviewing **one dimension** of this PR: whether its headline results already exist in Mathlib or in the pool. Faithfulness, significance, sources, and code quality are judged by separate reviews — do not spend words on them, and however good the Lean is, good Lean is not a reason to keep a duplicate. + +This dimension has been missed at real cost: #275 was approved with zero findings and closed by hand because its headline follows in a few lines from Mathlib's `SimpleGraph.nonempty_hom_of_forall_finite_subgraph_hom`, and #225 was closed as subsumed by the pool's own `Incompleteness` project. + +## What to judge + +A **Prior art** section above the diff carries a Mathlib search for every headline this PR adds, plus the complete list of pooled projects. Work from it: + +- For each headline, read the search hits against the claim. A hit is a *candidate*, not a verdict — shared vocabulary is not duplication. Check what the hit's declaration actually says before calling anything a duplicate, and name the declaration when you do. +- Compare against the pool list the same way. Prior art in the pool counts the same as prior art in Mathlib. +- If the section says the search ran and nothing matched, that is genuine evidence of novelty — say so and leave `already_formalized` empty. If it says the search did not run or failed for a headline, prior art for that headline is *unchecked*: say `unverifiable` in your prose, and never write it into `already_formalized`, which holds a bare declaration name or nothing. + +Not every overlap is duplication. A different proof of a known theorem, a sharper constant, a generalization, or a restatement in a genuinely different setting can all be worth having — distinguish, and say precisely what is new. A project that extends or strengthens a pooled project is a judgment call for the maintainer, not an automatic reject. + +## Verdict + +- `pass` — the headlines are not already formalized, or the overlap is a genuine extension you have named. +- `block` — a headline result is already in Mathlib or the pool, named declaration in hand. +- `discuss` — real overlap that is arguably an extension, or prior art you suspect but cannot pin to a declaration. + +## Output + +Return a single JSON object: + +```json +{ + "verdict": "pass" | "block" | "discuss", + "bottom_line": "", + "already_formalized": "", + "novelty_note": "", + "findings": [ + { + "file": "", + "line": , + "rule": "", + "comment": "", + "evidence": "" + } + ] +} +``` diff --git a/.github/review-rubrics/quality.md b/.github/review-rubrics/quality.md new file mode 100644 index 0000000000..4280090eb7 --- /dev/null +++ b/.github/review-rubrics/quality.md @@ -0,0 +1,52 @@ +# Rubric: quality — is the Lean good enough to maintain? + +You are reviewing **one dimension** of this PR: code quality. Faithfulness, novelty, significance, and sources are judged by separate reviews — do not spend words on them. + +This rubric is **advisory**: it cannot block a merge on its own. Your `block` is recorded as `discuss` — flag what a maintainer should weigh, and let them weigh it. The bar is "materially better than typical AI-agent slop", not mathlib-perfect. Half the pool is AI-written and the good ones are indistinguishable from human work; judge the artifact, not the provenance. + +The build, linters, and axiom audit already passed — never report a proof as broken. Style mechanics (headers, naming, line length, `simp` vs `simp only`, docstring presence) are caught elsewhere; do not flag them. + +## What to look for + +Patterns that survive a green build: + +- Walls of repeated `have`s, dead branches, term-mode where one tactic line works. +- Instances and structures with no consumer in the PR. +- Hypotheses a theorem never uses, or typeclass assumptions far stronger than the proof needs (`[Field F]` where `[Semiring R]` would do). +- Near-duplicate definitions of the same object under two names, or a lemma restated with the arguments permuted. +- Imports and `open`s with nothing to do with the subject — residue from an `exact?` search. +- `@[simp]` on a lemma whose left-hand side is not in simp-normal form. +- A linter or elaboration problem suppressed rather than fixed — `set_option linter.X false` in project code hides the thing the linter found, even where the option is permitted. + +## Scoring + +`code_quality` runs 1–5: 1 = clear AI slop, 3 = competent, 5 = mathlib-merge-ready. Any score other than 3 needs a finding or the bottom line to point at what earned it. Use the whole scale — a wall of dead `have`s is a 1 or 2, and saying 3 out of politeness helps nobody. + +## Verdict + +- `pass` — competent or better; nothing a maintainer must weigh. +- `discuss` — slop or debt bad enough that a human should look before merging. +- (`block` is recorded as `discuss` — this dimension advises, it does not veto.) + +## Output + +Return a single JSON object: + +```json +{ + "verdict": "pass" | "discuss", + "bottom_line": "", + "code_quality": , + "findings": [ + { + "file": "", + "line": , + "rule": "", + "comment": "", + "evidence": "" + } + ] +} +``` + +Having found one instance of a defect, look for the others and list them together rather than filing the first one you saw. diff --git a/.github/review-rubrics/significance.md b/.github/review-rubrics/significance.md new file mode 100644 index 0000000000..206fe4fbcc --- /dev/null +++ b/.github/review-rubrics/significance.md @@ -0,0 +1,60 @@ +# Rubric: significance — is this worth having? + +You are reviewing **one dimension** of this PR: whether the mathematics (or computer science, physics, game theory — a quarter of the pool is not pure mathematics, judged by its own field's standards) is worth pooling. Faithfulness, novelty, sources, and code quality are judged by separate reviews — do not spend words on them. + +## What we want + +- **Completed, self-contained projects.** A clear main theorem or set of theorems, proven within the PR. +- **Significance.** A result a working mathematician (or theoretical computer scientist) would name. Graduate or research level. +- **Theory building.** We prefer formalizations that develop a piece of mathematics over ad-hoc problem-solving on isolated obscure problems. Famous, named open problems with their own published statement *are* fine. + +## What we don't want + +- Single utility lemmas of any size, no matter how technical the proof. ("PMF.binomial_add_binomial" with a 160-line proof is still one utility lemma.) +- Random API generalizations or refactors with no headline result — what's the *theorem*? +- Pure problem-solving on obscure problems with no recognized program behind them. +- Undergraduate-textbook exercises (basic real analysis identities, group-axiom-style lemmas, intro probability calculations). +- **Bulk that someone else has to maintain.** Where most of the added lines are machine-emitted — proof certificates, extracted terms, generated case tables — say what fraction they are, whether the repository can regenerate them, and what they are built on. Generated bulk riding an internal or unstable Mathlib API turns every version bump into a regeneration liability, and that cost lands on the pool. + +## Calibration + +The median pooled project is ~2,800 lines of Lean, the tenth percentile ~900, and only four of 138 are under 500. Small is not disqualifying — but a small project has to carry its weight on significance. + +**Worth having:** `clawristotle` (Vlasov-Maxwell-Landau steady-state classification, ~10K LOC, paper-anchored); `formal-learning-theory` (~19K LOC, several named theorems); `hadwiger-nelson-bounds` (kernel-checked 5 ≤ χ(ℝ²) ≤ 7 — a named open problem honestly bounded); `erdos132-n14` (~2K LOC conditional case of Erdős 132, conditionality disclosed); `sensitivity`, `circuit-complexity`, `pumping-cfg` (theoretical CS at the same bar). + +**Not worth having:** two trivial binomial-PMF corollaries; an additive-convolution API generalization with no headline; a 176-line single-lemma PR proving an undergrad probability identity, however gnarly the proof. + +## When there is no project to judge + +A mixed PR can arrive with no new project in it — a Mathlib bump repairing every library, a CI change touching a pooled file, a project removal. Do not force it through this rubric: set `fit` to `not_applicable`, say in one sentence what the PR does, and `pass` unless something in the pooled Lean it touches is objectionable on this dimension. + +## Verdict + +- `pass` — graduate-or-research-level content a mathematician would name, or `not_applicable`. +- `block` — undergraduate exercise, utility lemma, no headline result, or unmaintainable generated bulk. +- `discuss` — genuinely borderline: real but modest content, or generated bulk whose maintenance price a human should weigh. + +## Output + +Return a single JSON object: + +```json +{ + "verdict": "pass" | "block" | "discuss", + "bottom_line": "", + "fit": "good_fit" | "borderline" | "not_a_fit" | "not_applicable", + "level": "undergraduate" | "graduate" | "research", + "branch": "", + "mode": "theory_building" | "problem_solving" | "mixed", + "significance_one_sentence": "", + "findings": [ + { + "file": "", + "line": , + "rule": "", + "comment": "", + "evidence": "" + } + ] +} +``` diff --git a/.github/review-rubrics/sources.md b/.github/review-rubrics/sources.md new file mode 100644 index 0000000000..de9ff4d914 --- /dev/null +++ b/.github/review-rubrics/sources.md @@ -0,0 +1,40 @@ +# Rubric: sources — does the citation say what the PR says it says? + +You are reviewing **one dimension** of this PR: whether its cited sources support its claims, and whether prior work is credited. Faithfulness, novelty, significance, and code quality are judged by separate reviews — do not spend words on them. + +The *presence* of a source is gated deterministically; never flag a missing or misplaced YAML field. Your question is whether the source that is there **holds up**. + +## What to judge + +- **Does the cited work state the cited result?** Right theorem, right hypotheses, right attribution. Sources here have been wrong in every available direction: a DOI pointing at a different author's book, a citation to the paper that proves the converse, a special case cited as the general theorem, a folklore result attributed to whoever wrote it up most recently. +- **Labelled differences.** A project may knowingly prove a generalization, special case, or variant of the cited theorem — fine, and often the point. What is not fine is presenting it as the cited result. Ask that the difference be labelled, not removed. +- **Uncredited prior formalizations.** Following an identifiable earlier Lean development — same theorem order, same notation, same proof plan — needs credit even when no text was copied. + +You usually cannot fetch the source. Judge from what the diff shows: the card's citation text, docstrings quoting the source's statement, and internal consistency between them. When the diff does not let you verify, say `unverifiable` — that is a normal outcome, not a defect, and it is not grounds for blocking on its own. + +## Verdict + +- `pass` — citations are consistent with what the project claims, or honestly `unverifiable` with nothing suspicious. +- `block` — the source demonstrably does not say what the PR says it says, or prior formalization work is knowingly passed off as original. +- `discuss` — an inconsistency you can point at but not settle from the diff. + +## Output + +Return a single JSON object: + +```json +{ + "verdict": "pass" | "block" | "discuss", + "bottom_line": "", + "source_match": "matches" | "mismatch" | "unverifiable" | "not_a_known_result", + "findings": [ + { + "file": "", + "line": , + "rule": "", + "comment": "", + "evidence": "" + } + ] +} +``` diff --git a/python/lean_pool/review.py b/python/lean_pool/review.py index 5c364bd636..4a3db38b8b 100644 --- a/python/lean_pool/review.py +++ b/python/lean_pool/review.py @@ -2,8 +2,13 @@ Detects what kind of PR this is and reviews it under the matching rules: -- **project** — adds a new project to the pool. Judged on fit and - significance (``.github/REVIEW_RULES.md``). +- **project** — adds a new project to the pool. Reviewed once per + rubric — faithfulness, novelty, significance, sources, and advisory + code quality (``.github/review-rubrics/``), each an independent model + call on top of the shared core (``.github/REVIEW_RULES.md``). The + overall verdict is computed from the rubric verdicts, never asked of + a model: any blocking ``block`` → request_changes, any ``discuss`` → + needs_discussion, and an elided-diff review cannot approve. - **refactor** — only touches projects already in the pool, the same added-vs-modified split ``/profile`` uses. Judged on tech debt and maintainability (``.github/REFACTOR_REVIEW_RULES.md``). @@ -241,38 +246,6 @@ def pricing_rates( TAMPERING_ICON = {True: "🛑", False: "✅"} HOLE_RISK_ICON = {"none": "✅", "review_needed": "🟡", "gamed": "🛑"} -SYSTEM_PROMPT_PROJECT = dedent( - """\ - You are a senior mathematician and Lean engineer reviewing pull - requests to Lean Pool, a curated repository of formalization - projects — mathematics and the disciplines next to it, so about a - quarter of the pool is theoretical computer science, information - theory, mathematical physics, and game theory. Your job is to tell - the maintainer, in one paragraph plus a short structured assessment, - whether this PR is worth merging. - - Write to a colleague: direct, no encouragement, no editorializing, - no convention justifications, no "great work." - - The build, the linters, and the axiom audit have already passed — - assume that, and never report a proof as broken or incomplete. - Mechanical style issues (sorry, headers, naming, simp discipline, - line length, card schema) are caught elsewhere in CI. Do NOT flag - those, even if you notice them. - - What the gates cannot check is whether the project proves what its - card claims, what it assumes rather than proves, whether someone has - already done it, and whether its cited source supports it. That is - the review. Much of what you read was written by an AI and reads - fluently whether or not it is right, so rest every claim on the Lean - itself rather than on a docstring that asserts it. - - Always respond with a single JSON object matching the schema in the - rules document. The `assessment` block is the core deliverable — - that is what tells the maintainer whether to bother reading the PR. - """ -) - SYSTEM_PROMPT_REFACTOR = dedent( """\ You are a senior Lean engineer reviewing a refactor pull request to @@ -411,13 +384,79 @@ def pricing_rates( ) # Rules document and system prompt per PR kind, keyed by `classify_pr`. +# Project PRs do not appear here: they are reviewed per-rubric (see +# PROJECT_RUBRICS) rather than in one monolithic call. REVIEW_MODES: dict[str, tuple[Path, str]] = { - "project": (PROJECT_RULES_PATH, SYSTEM_PROMPT_PROJECT), "refactor": (REFACTOR_RULES_PATH, SYSTEM_PROMPT_REFACTOR), "challenge": (CHALLENGE_RULES_PATH, SYSTEM_PROMPT_CHALLENGE), "solution": (SOLUTION_RULES_PATH, SYSTEM_PROMPT_SOLUTION), } +RUBRICS_DIR = REPO_ROOT / ".github" / "review-rubrics" + + +@dataclass(frozen=True) +class RubricSpec: + """One dimension a project PR is reviewed on, by its own model call. + + An audit of the 148 monolithic reviews showed one narrative call + letting a positive overall impression swamp specific checks — the + two worst misses (#275, #278) were long approving summaries with + zero findings. Tau Ceti's review runs each angle as its own agent + for exactly this reason; this is that structure, sized to the pool. + + Attributes: + key: Verdict-table identifier, also the rubric filename stem. + title: Human-readable rubric name for the comment. + blocking: Whether this rubric's ``block`` can force + ``request_changes``. An advisory rubric's ``block`` is + recorded as ``discuss`` — it informs, it does not veto. + wants_prior_art: Whether the pre-computed Mathlib/pool search + evidence is included in this rubric's prompt. + """ + + key: str + title: str + blocking: bool + wants_prior_art: bool = False + + @property + def path(self) -> Path: + """The rubric's markdown file under ``.github/review-rubrics/``.""" + return RUBRICS_DIR / f"{self.key}.md" + + +# Ordered by expected value per token: the dimensions that have actually +# rejected PRs first. `quality` is advisory — in 148 reviews it produced +# one finding and never drove a verdict, so it flags for a human rather +# than vetoing. +PROJECT_RUBRICS: list[RubricSpec] = [ + RubricSpec("faithfulness", "Faithfulness", blocking=True), + RubricSpec("novelty", "Novelty", blocking=True, wants_prior_art=True), + RubricSpec("significance", "Significance", blocking=True), + RubricSpec("sources", "Sources", blocking=True), + RubricSpec("quality", "Code quality", blocking=False), +] + +SYSTEM_PROMPT_RUBRIC = dedent( + """\ + You are a senior mathematician and Lean engineer reviewing ONE + dimension of a pull request to Lean Pool, a curated repository of + formalization projects. The rules document below names your + dimension and ends with your output schema. Other dimensions are + reviewed by separate, independent reviews — stay inside yours, and + do not let strength or weakness elsewhere move your verdict. + + Write to a colleague: direct, no encouragement, no editorializing. + The build, linters, and axiom audit already passed; never report a + proof as broken. Rest every claim on the Lean in the diff, not on + prose that asserts it. + + Always respond with a single JSON object matching the schema in the + rules document. + """ +) + def run_gh(*args: str, stdin: str | None = None) -> str: """Run ``gh`` with the given arguments and return stdout. @@ -1138,6 +1177,89 @@ def request_review( raise RuntimeError("unreachable: review fit loop exited without a result") +@dataclass(frozen=True) +class RubricOutcome: + """One rubric's completed review of a project PR. + + Attributes: + spec: The rubric that ran. + result: The underlying model call. + verdict: Normalized to ``pass`` / ``block`` / ``discuss`` — + see :func:`normalize_rubric_verdict`. + """ + + spec: RubricSpec + result: ReviewResult + verdict: str + + +def normalize_rubric_verdict(spec: RubricSpec, payload: dict) -> str: + """Clamp a rubric's self-reported verdict to what it may say. + + An advisory rubric's ``block`` becomes ``discuss`` — it informs the + maintainer, it does not veto. Anything unrecognized also becomes + ``discuss``: a review whose verdict cannot be read is a review a + human should look at, never a silent pass. + """ + verdict = (payload.get("verdict") or "").strip() + if verdict not in ("pass", "block", "discuss"): + return "discuss" + if verdict == "block" and not spec.blocking: + return "discuss" + return verdict + + +def aggregate_verdict(outcomes: list[RubricOutcome], truncated: bool) -> str: + """Compute the overall verdict from the rubric outcomes. + + The model is never asked for an overall verdict — the audit showed + `fit` ~96% collinear with the verdict it sat next to, i.e. the + narrative was grading itself. Deterministic aggregation also + enforces what a prompt can only request: a partial (elided-diff) + review cannot approve, because nobody read the elided files. + """ + if any(outcome.verdict == "block" for outcome in outcomes): + return "request_changes" + if truncated or any(outcome.verdict == "discuss" for outcome in outcomes): + return "needs_discussion" + return "approve" + + +def run_project_rubrics( + model: str, + diff: str, + effort: str | None, + context: PullRequestContext | None, + prior_art_section: str | None, +) -> list[RubricOutcome]: + """Review a project PR once per rubric in :data:`PROJECT_RUBRICS`. + + Every call shares the same core rules, PR context, and diff; only + the rubric text differs, plus the prior-art evidence for the rubric + that judges novelty. Calls run sequentially — flex-tier latency is + acceptable for a comment bot, and sequencing keeps the tier and + overflow fallbacks per call untouched. + """ + core = PROJECT_RULES_PATH.read_text(encoding="utf-8") + outcomes: list[RubricOutcome] = [] + for spec in PROJECT_RUBRICS: + rules = f"{core}\n\n---\n\n{spec.path.read_text(encoding='utf-8')}" + print(f"Rubric {spec.key}: requesting review.", file=sys.stderr) + result = request_review( + model=model, + rules=rules, + diff=diff, + system_prompt=SYSTEM_PROMPT_RUBRIC, + effort=effort, + context=context, + prior_art_section=prior_art_section if spec.wants_prior_art else None, + ) + verdict = normalize_rubric_verdict(spec, result.payload) + print(f"Rubric {spec.key}: {verdict}.", file=sys.stderr) + outcomes.append(RubricOutcome(spec=spec, result=result, verdict=verdict)) + return outcomes + + def render_usage(usage: Any, model: str, tier: str, effort: str | None = None) -> str: """Render a one-line token / tier / effort / cost footer. @@ -1167,58 +1289,6 @@ def render_usage(usage: Any, model: str, tier: str, effort: str | None = None) - return " · ".join(parts) -def render_project_assessment(payload: dict) -> str: - """Render a new-project assessment block as a Markdown table. - - The rows the maintainer has to act on come first: whether the Lean - proves what the card claims, whether the cited source backs it, what - it assumes, and whether someone has already done it. Fit and level - sit below — the verdict is rendered directly above this table and - ``fit`` almost always restates it. - """ - a = payload.get("assessment") or {} - if not a: - return "" - - fit = a.get("fit", "") - fit_cell = f"{FIT_ICON.get(fit, '•')} `{fit}`" if fit else "?" - quality = a.get("code_quality") - quality_cell = f"{quality} / 5" if quality is not None else "?" - - rows = [ - ("Proves the claim", _icon_cell(CLAIM_ICON, a.get("proves_the_claim", ""))), - ( - "Matches cited source", - _icon_cell(SOURCE_MATCH_ICON, a.get("source_match", "")), - ), - ] - already = (a.get("already_formalized") or "").strip() - if already: - rows.append(("Already formalized", _prior_art_cell(already))) - assumed = (a.get("assumed_inputs") or "").strip() - if assumed: - rows.append(("Assumed, not proved", assumed)) - rows += [ - ("Fit", fit_cell), - ("Level", f"`{a.get('level', '?')}`"), - ("Branch", a.get("branch", "?")), - ("Mode", f"`{a.get('mode', '?')}`"), - ("Code quality", quality_cell), - ] - - table = "| Aspect | Value |\n|---|---|\n" - for k, v in rows: - table += f"| {k} | {v} |\n" - - note = (a.get("claim_note") or "").strip() - if note: - table += f"\n**Statement check:** {note}\n" - sig = (a.get("significance_one_sentence") or "").strip() - if sig: - table += f"\n_{sig}_" - return table - - def render_refactor_assessment(payload: dict) -> str: """Render a refactor assessment block as a Markdown table.""" a = payload.get("assessment") or {} @@ -1349,6 +1419,181 @@ def render_solution_assessment(payload: dict) -> str: return table +RUBRIC_VERDICT_ICON = {"pass": "✅", "block": "🛑", "discuss": "🤔"} + + +def _rubric_facts_table(outcomes: list[RubricOutcome]) -> str: + """Assemble the key structured fields across rubrics into one table.""" + payloads = {outcome.spec.key: outcome.result.payload for outcome in outcomes} + + def field(key: str, name: str) -> str: + return str(payloads.get(key, {}).get(name) or "").strip() + + rows: list[tuple[str, str]] = [] + claim = field("faithfulness", "proves_the_claim") + if claim: + rows.append(("Proves the claim", _icon_cell(CLAIM_ICON, claim))) + assumed = field("faithfulness", "assumed_inputs") + if assumed: + rows.append(("Assumed, not proved", assumed)) + already = field("novelty", "already_formalized") + if already: + rows.append(("Already formalized", _prior_art_cell(already))) + source = field("sources", "source_match") + if source: + rows.append(("Matches cited source", _icon_cell(SOURCE_MATCH_ICON, source))) + fit = field("significance", "fit") + if fit: + rows.append(("Fit", _icon_cell(FIT_ICON, fit))) + for key, label in (("level", "Level"), ("branch", "Branch"), ("mode", "Mode")): + value = field("significance", key) + if value: + rows.append((label, f"`{value}`" if key != "branch" else value)) + quality = payloads.get("quality", {}).get("code_quality") + if quality is not None: + rows.append(("Code quality", f"{quality} / 5")) + if not rows: + return "" + table = "| Aspect | Value |\n|---|---|\n" + for name, value in rows: + table += f"| {name} | {value} |\n" + claim_note = field("faithfulness", "claim_note") + if claim_note: + table += f"\n**Statement check:** {claim_note}\n" + significance = field("significance", "significance_one_sentence") + if significance: + table += f"\n_{significance}_" + return table + + +def _render_rubric_usage(outcomes: list[RubricOutcome], effort: str | None) -> str: + """Sum tokens and cost across the rubric calls into one footer line.""" + in_tokens = 0 + out_tokens = 0 + cost = 0.0 + unpriced = False + for outcome in outcomes: + usage = outcome.result.usage + if usage is None: + unpriced = True + continue + call_in = getattr(usage, "prompt_tokens", 0) or 0 + call_out = getattr(usage, "completion_tokens", 0) or 0 + in_tokens += call_in + out_tokens += call_out + rates = pricing_rates(outcome.result.model, outcome.result.tier, call_in) + if rates is None: + unpriced = True + continue + cost += (call_in * rates[0] + call_out * rates[1]) / 1_000_000 + parts = [ + f"**Tokens:** {in_tokens:,} in / {out_tokens:,} out " + f"across {len(outcomes)} rubric calls" + ] + if effort: + parts.append(f"**Effort:** `{effort}`") + cost_cell = f"**Cost:** ${cost:.4f}" + if unpriced: + cost_cell += " (partial — some calls unpriced)" + parts.append(cost_cell) + return " · ".join(parts) + + +def render_rubric_comment( + outcomes: list[RubricOutcome], + verdict: str, + model: str, + reviewed_head_sha: str, + effort: str | None = None, +) -> str: + """Render the combined per-rubric review as one sticky PR comment.""" + lines = [ + LLM_REVIEW_MARKER, + f"## 🤖 LLM review (`{model}`, {len(outcomes)} rubrics)", + "", + ] + if reviewed_head_sha: + lines.extend([f"**Reviewed head:** `{reviewed_head_sha}`", ""]) + + truncation = next( + (o.result.truncation for o in outcomes if o.result.truncation is not None), + None, + ) + if truncation is not None: + lines.extend( + [ + "> ⚠️ **Partial review — diff exceeded the size budget.** The " + f"bodies of the {truncation.elided_files} largest of " + f"{truncation.total_files} file patches were elided before " + "review; an elided review cannot approve.", + "", + ] + ) + + icon = VERDICT_ICON.get(verdict, "•") + lines.extend( + [ + f"**Verdict:** {icon} `{verdict}` — computed from the rubric " + "verdicts below, not chosen by a model.", + "", + "| Rubric | Verdict | Bottom line |", + "|---|---|---|", + ] + ) + for outcome in outcomes: + rubric_icon = RUBRIC_VERDICT_ICON.get(outcome.verdict, "•") + bottom = str(outcome.result.payload.get("bottom_line") or "").strip() + advisory = "" if outcome.spec.blocking else " _(advisory)_" + lines.append( + f"| {outcome.spec.title}{advisory} | {rubric_icon} " + f"`{outcome.verdict}` | {bottom} |" + ) + lines.append("") + + facts = _rubric_facts_table(outcomes) + if facts: + lines.extend([facts, ""]) + + for outcome in outcomes: + findings = outcome.result.payload.get("findings") or [] + if not findings: + continue + lines.append(f"### {outcome.spec.title} findings ({len(findings)})") + lines.append("") + for finding in findings: + path = finding.get("file") or "" + line_no = finding.get("line", 0) or 0 + if path and line_no: + ref = f"`{path}:{line_no}`" + elif path: + ref = f"`{path}`" + else: + ref = "_PR-wide_" + lines.append(f"- **{finding.get('rule', '')}** — {ref}") + body = (finding.get("comment") or "").strip() + lines.append(f" {body}") + evidence = (finding.get("evidence") or "").strip() + if evidence: + lines.append(f" _Evidence:_ {evidence}") + lines.append("") + + lines.append("---") + lines.append(_render_rubric_usage(outcomes, effort)) + lines.append( + "_Each rubric is an independent review against " + "[`.github/review-rubrics/`](../blob/main/.github/review-rubrics) " + "on top of [`.github/REVIEW_RULES.md`](../blob/main/.github/REVIEW_RULES.md). " + "Disagree? Reply on the PR; rules can be updated in a PR of their own._" + ) + if verdict == "request_changes": + lines.append( + "_`request_changes` is an ask, not a close: of the reviewer's past " + "`request_changes` verdicts, 39% were merged after a human looked. " + "Read the findings before acting on the verdict._" + ) + return "\n".join(lines) + + def render_comment( payload: dict, model: str, @@ -1409,7 +1654,7 @@ def render_comment( "challenge": render_challenge_assessment, "solution": render_solution_assessment, } - assessment = renderers.get(kind, render_project_assessment)(payload) + assessment = renderers.get(kind, lambda _payload: "")(payload) if assessment: lines.extend([assessment, ""]) @@ -1648,9 +1893,6 @@ def main() -> int: ) return 0 - rules_path, system_prompt = REVIEW_MODES[kind] - rules = rules_path.read_text(encoding="utf-8") - if kind == "solution": reason = solution_needs_llm_review(files, REPO_ROOT) if reason is None: @@ -1672,6 +1914,29 @@ def main() -> int: if not diff.strip(): print("Empty diff; nothing to review.", file=sys.stderr) return 0 + + if kind == "project": + outcomes = run_project_rubrics( + model=model, + diff=diff, + effort=effort, + context=fetch_pr_context(pr_number, repo_full_name), + prior_art_section=gather_prior_art(kind, reviewed_head_sha, repo_full_name), + ) + truncated = any(o.result.truncation is not None for o in outcomes) + verdict = aggregate_verdict(outcomes, truncated) + comment = render_rubric_comment( + outcomes, + verdict=verdict, + model=outcomes[0].result.model, + reviewed_head_sha=reviewed_head_sha, + effort=outcomes[0].result.effort, + ) + post_comment(pr_number, comment, repo_full_name=repo_full_name) + return 0 + + rules_path, system_prompt = REVIEW_MODES[kind] + rules = rules_path.read_text(encoding="utf-8") result = request_review( model=model, rules=rules, diff --git a/python/tests/test_review.py b/python/tests/test_review.py index 55ecda40e9..64a3ef9ae8 100644 --- a/python/tests/test_review.py +++ b/python/tests/test_review.py @@ -911,85 +911,190 @@ def test_fetch_pr_context_tolerates_a_null_description(monkeypatch) -> None: assert review.fetch_pr_context("1", "o/r").body == "" -def test_project_assessment_leads_with_the_ungated_checks() -> None: - """Claim, source, and prior art outrank the fields that echo the verdict.""" - from lean_pool.review import render_project_assessment +def _outcome(key, verdict="pass", payload=None, usage=None): + """Build one RubricOutcome for rendering/aggregation tests.""" + from lean_pool import review - table = render_project_assessment( - { - "assessment": { - "fit": "borderline", - "level": "research", - "branch": "graph theory", - "mode": "theory_building", - "proves_the_claim": "weaker_than_claimed", - "claim_note": "Proved for n = 14 only, not all n.", - "assumed_inputs": "Szöllősi–Östergård classification, disclosed", - "already_formalized": "SimpleGraph.nonempty_hom_of_forall_finite", - "source_match": "matches", - "code_quality": 4, - "significance_one_sentence": "A conditional fourteen-point case.", - } - } + spec = next(s for s in review.PROJECT_RUBRICS if s.key == key) + result = review.ReviewResult( + payload=payload or {"verdict": verdict, "bottom_line": f"{key} fine."}, + usage=usage, + tier="flex", + truncation=None, + model="gpt-5.6-sol-2026-06-17", + effort="xhigh", ) + return review.RubricOutcome(spec=spec, result=result, verdict=verdict) - assert "Proves the claim" in table - assert "weaker_than_claimed" in table - assert "Proved for n = 14 only" in table - assert "Already formalized" in table - assert "Assumed, not proved" in table - assert "Szöllősi–Östergård" in table - # The ungated checks lead; `fit` and `level` echo the verdict that is - # already rendered above the table, so they come last. - assert table.index("Proves the claim") < table.index("| Fit |") - assert table.index("Already formalized") < table.index("| Fit |") - assert table.index("Assumed, not proved") < table.index("| Fit |") - assert table.index("| Fit |") < table.index("| Level |") - # The field that was `no` in all 147 past reviews is gone. - 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"}} +def test_advisory_rubric_block_is_recorded_as_discuss() -> None: + """Code quality informs the maintainer; it does not veto a merge.""" + from lean_pool import review + + quality = next(s for s in review.PROJECT_RUBRICS if not s.blocking) + faithfulness = next(s for s in review.PROJECT_RUBRICS if s.blocking) + + assert review.normalize_rubric_verdict(quality, {"verdict": "block"}) == "discuss" + assert ( + review.normalize_rubric_verdict(faithfulness, {"verdict": "block"}) == "block" ) - hit = render_project_assessment( - {"assessment": {"already_formalized": "SimpleGraph.nonempty_hom"}} + # An unreadable verdict is a review for a human, never a silent pass. + assert review.normalize_rubric_verdict(faithfulness, {}) == "discuss" + assert ( + review.normalize_rubric_verdict(faithfulness, {"verdict": "approve"}) + == "discuss" ) - assert "🛑" not in hedged - assert "🟡 unverifiable from the supplied diff" in hedged - assert "🛑 `SimpleGraph.nonempty_hom`" in hit +def test_aggregate_verdict_is_deterministic() -> None: + """Block beats discuss beats pass, and a partial diff cannot approve.""" + from lean_pool.review import aggregate_verdict -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 + all_pass = [_outcome("faithfulness"), _outcome("novelty")] + one_block = [_outcome("faithfulness", "block"), _outcome("novelty")] + one_discuss = [_outcome("faithfulness"), _outcome("quality", "discuss")] - table = render_project_assessment( - { - "assessment": { - "fit": "good_fit", - "level": "research", + assert aggregate_verdict(all_pass, truncated=False) == "approve" + assert aggregate_verdict(one_block, truncated=False) == "request_changes" + assert aggregate_verdict(one_discuss, truncated=False) == "needs_discussion" + # Nobody read the elided files, so clean rubrics still cannot approve. + assert aggregate_verdict(all_pass, truncated=True) == "needs_discussion" + assert aggregate_verdict(one_block, truncated=True) == "request_changes" + + +def test_rubric_comment_carries_table_facts_and_findings() -> None: + """The combined comment shows each rubric, the facts, and evidence.""" + from lean_pool.review import render_rubric_comment + + outcomes = [ + _outcome( + "faithfulness", + payload={ + "verdict": "pass", + "bottom_line": "Headline matches the card.", "proves_the_claim": "proves_it", - "already_formalized": "", + "claim_note": "Proves the n = 14 case exactly as stated.", "assumed_inputs": "", - "code_quality": 4, - } - } + "findings": [], + }, + ), + _outcome( + "novelty", + verdict="block", + payload={ + "verdict": "block", + "bottom_line": "Already in Mathlib.", + "already_formalized": "SimpleGraph.nonempty_hom", + "findings": [ + { + "file": "LeanPool/X/A.lean", + "line": 12, + "rule": "duplicate-of-mathlib", + "comment": "The headline follows from Finsubgraph.", + "evidence": "SimpleGraph.nonempty_hom states the same.", + } + ], + }, + ), + _outcome("quality", verdict="discuss"), + ] + + body = render_rubric_comment( + outcomes, + verdict="request_changes", + model="gpt-5.6-sol-2026-06-17", + reviewed_head_sha="abc123", + effort="xhigh", + ) + + assert body.startswith("") + assert "**Reviewed head:** `abc123`" in body + assert "computed from the rubric verdicts" in body + assert "| Faithfulness | " in body and "| Novelty | " in body + assert "Code quality _(advisory)_" in body + assert "🛑 `SimpleGraph.nonempty_hom`" in body + assert "### Novelty findings (1)" in body + assert "_Evidence:_ SimpleGraph.nonempty_hom states the same." in body + assert "an ask, not a close" in body + assert "review-rubrics" in body + + +def test_rubric_facts_render_a_prior_art_hedge_as_a_hedge() -> None: + """Prose in already_formalized must not wear the duplicate stop icon.""" + from lean_pool.review import _rubric_facts_table + + hedged = _rubric_facts_table( + [ + _outcome( + "novelty", + payload={ + "verdict": "pass", + "already_formalized": "unverifiable from the supplied diff", + }, + ) + ] + ) + + assert "🛑" not in hedged + assert "🟡 unverifiable from the supplied diff" in hedged + + +def test_run_project_rubrics_isolates_the_angles(monkeypatch, tmp_path) -> None: + """Each rubric gets the core plus its own file; only novelty gets search.""" + from lean_pool import review + + calls: list[dict] = [] + + def _fake_request_review(**kwargs): + calls.append(kwargs) + return review.ReviewResult( + payload={"verdict": "pass", "bottom_line": "ok"}, + usage=None, + tier="flex", + truncation=None, + model="gpt-5.6-sol", + effort="xhigh", + ) + + monkeypatch.setattr(review, "request_review", _fake_request_review) + + outcomes = review.run_project_rubrics( + model="gpt-5.6", + diff="diff --git a/x b/x", + effort="xhigh", + context=None, + prior_art_section="PRIOR-ART-EVIDENCE", ) - assert "Already formalized" not in table - assert "Assumed, not proved" not in table - assert "✅ `proves_it`" in table + assert [o.spec.key for o in outcomes] == [s.key for s in review.PROJECT_RUBRICS] + by_key = dict(zip([s.key for s in review.PROJECT_RUBRICS], calls, strict=True)) + # Every call shares the core rules and carries its own rubric. + for key, call in by_key.items(): + assert "shared core" in call["rules"] + assert f"Rubric: {key}" in call["rules"] + assert call["system_prompt"] == review.SYSTEM_PROMPT_RUBRIC + # The search evidence goes only to the rubric that judges novelty. + assert by_key["novelty"]["prior_art_section"] == "PRIOR-ART-EVIDENCE" + assert by_key["faithfulness"]["prior_art_section"] is None + assert by_key["quality"]["prior_art_section"] is None + + +def test_rubric_usage_sums_cost_across_calls() -> None: + """The footer prices each call at its own tier and adds them up.""" + from lean_pool.review import _render_rubric_usage + + usage = types.SimpleNamespace(prompt_tokens=10_000, completion_tokens=2_000) + outcomes = [ + _outcome("faithfulness", usage=usage), + _outcome("novelty", usage=usage), + ] + + line = _render_rubric_usage(outcomes, "xhigh") + + assert "20,000 in / 4,000 out across 2 rubric calls" in line + assert "**Effort:** `xhigh`" in line + # 2 x (10k x $2.50/M + 2k x $15/M) = 2 x $0.055 = $0.11 on flex. + assert "**Cost:** $0.1100" in line def test_request_changes_comment_says_it_is_not_a_close() -> None: From 62405e8eb566980357b2aa39bb81e63ec5cf449d Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Wed, 29 Jul 2026 01:16:19 -0700 Subject: [PATCH 2/2] Show the tier, price honestly, and keep quality.md consistent Greptile on #313: the rubric footer omitted the tier every single-call footer shows (five calls can land on different tiers, which is exactly when it matters); an entirely unpriced run rendered $0.0000, which reads as free rather than unknown; an empty finding comment emitted a bare two-space line; and quality.md's Verdict prose offered a `block` its own schema does not, so a careful model and a schema-following one would answer differently. All four fixed; the advisory rubric now says plainly it has no block. Co-Authored-By: Claude Fable 5 --- .github/review-rubrics/quality.md | 5 +++-- python/lean_pool/review.py | 19 +++++++++++++------ python/tests/test_review.py | 11 +++++++++++ 3 files changed, 27 insertions(+), 8 deletions(-) diff --git a/.github/review-rubrics/quality.md b/.github/review-rubrics/quality.md index 4280090eb7..7033d3e34f 100644 --- a/.github/review-rubrics/quality.md +++ b/.github/review-rubrics/quality.md @@ -2,7 +2,7 @@ You are reviewing **one dimension** of this PR: code quality. Faithfulness, novelty, significance, and sources are judged by separate reviews — do not spend words on them. -This rubric is **advisory**: it cannot block a merge on its own. Your `block` is recorded as `discuss` — flag what a maintainer should weigh, and let them weigh it. The bar is "materially better than typical AI-agent slop", not mathlib-perfect. Half the pool is AI-written and the good ones are indistinguishable from human work; judge the artifact, not the provenance. +This rubric is **advisory**: it cannot block a merge on its own — flag what a maintainer should weigh, and let them weigh it. The bar is "materially better than typical AI-agent slop", not mathlib-perfect. Half the pool is AI-written and the good ones are indistinguishable from human work; judge the artifact, not the provenance. The build, linters, and axiom audit already passed — never report a proof as broken. Style mechanics (headers, naming, line length, `simp` vs `simp only`, docstring presence) are caught elsewhere; do not flag them. @@ -24,9 +24,10 @@ Patterns that survive a green build: ## Verdict +This dimension advises; it has no `block`. However bad the code, the worst you say is "a human should look." + - `pass` — competent or better; nothing a maintainer must weigh. - `discuss` — slop or debt bad enough that a human should look before merging. -- (`block` is recorded as `discuss` — this dimension advises, it does not veto.) ## Output diff --git a/python/lean_pool/review.py b/python/lean_pool/review.py index 4a3db38b8b..b5825e90c8 100644 --- a/python/lean_pool/review.py +++ b/python/lean_pool/review.py @@ -1486,16 +1486,22 @@ def _render_rubric_usage(outcomes: list[RubricOutcome], effort: str | None) -> s unpriced = True continue cost += (call_in * rates[0] + call_out * rates[1]) / 1_000_000 + tiers = dict.fromkeys(o.result.tier for o in outcomes if o.result.tier) + tier_cell = " / ".join(tiers) if tiers else "unknown" parts = [ f"**Tokens:** {in_tokens:,} in / {out_tokens:,} out " - f"across {len(outcomes)} rubric calls" + f"across {len(outcomes)} rubric calls", + f"**Tier:** `{tier_cell}`", ] if effort: parts.append(f"**Effort:** `{effort}`") - cost_cell = f"**Cost:** ${cost:.4f}" - if unpriced: - cost_cell += " (partial — some calls unpriced)" - parts.append(cost_cell) + if cost > 0 or not unpriced: + cost_cell = f"**Cost:** ${cost:.4f}" + if unpriced: + cost_cell += " (partial — some calls unpriced)" + parts.append(cost_cell) + else: + parts.append("_(no pricing recorded for these calls)_") return " · ".join(parts) @@ -1571,7 +1577,8 @@ def render_rubric_comment( ref = "_PR-wide_" lines.append(f"- **{finding.get('rule', '')}** — {ref}") body = (finding.get("comment") or "").strip() - lines.append(f" {body}") + if body: + lines.append(f" {body}") evidence = (finding.get("evidence") or "").strip() if evidence: lines.append(f" _Evidence:_ {evidence}") diff --git a/python/tests/test_review.py b/python/tests/test_review.py index 64a3ef9ae8..fabc6510d9 100644 --- a/python/tests/test_review.py +++ b/python/tests/test_review.py @@ -1092,11 +1092,22 @@ def test_rubric_usage_sums_cost_across_calls() -> None: line = _render_rubric_usage(outcomes, "xhigh") assert "20,000 in / 4,000 out across 2 rubric calls" in line + assert "**Tier:** `flex`" in line assert "**Effort:** `xhigh`" in line # 2 x (10k x $2.50/M + 2k x $15/M) = 2 x $0.055 = $0.11 on flex. assert "**Cost:** $0.1100" in line +def test_rubric_usage_without_pricing_says_so_instead_of_free() -> None: + """No usage data must read as unknown, not as $0.0000.""" + from lean_pool.review import _render_rubric_usage + + line = _render_rubric_usage([_outcome("faithfulness")], None) + + assert "$0.0000" not in line + assert "no pricing recorded" in line + + def test_request_changes_comment_says_it_is_not_a_close() -> None: """39% of past `request_changes` verdicts were merged after a human look.""" from lean_pool.review import render_comment