Make reviews decide and close PRs by age

.github/REFACTOR_REVIEW_RULES.md

@@ -74,7 +74,7 @@ Return a single JSON object:
     "risk": "low" | "medium" | "high",
     "assessment_one_sentence": "<one sentence: the bottom line for the maintainer>"
   },
-  "verdict": "approve" | "request_changes" | "needs_discussion",
+  "verdict": "approve" | "request_changes",
   "findings": [
     {
       "file": "<repo-relative path, or empty if PR-wide>",
@@ -96,9 +96,9 @@ Verdict mapping:
   maintainer needs to act on before merging.
 - `request_changes` — it introduces tech debt or brittleness serious enough
   that the maintainer should fix it (or ask the author to) before merging.
-- `needs_discussion` — a genuine trade-off the maintainer should weigh (e.g.
-  a large `simp_all` golf that is shorter and passes today but measurably more
-  fragile), where reasonable people could go either way.
+There is no third verdict; decide. For a genuine trade-off (e.g. a large
+`simp_all` golf that is shorter and passes today but measurably more fragile),
+pick the side the evidence favours and say why.
 
 ## Style
 

.github/REVIEW_RULES.md

@@ -4,7 +4,7 @@ You are reviewing a pull request to **Lean Pool**, a curated repository of forma
 
 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, Tau Ceti, 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 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.
+The overall verdict is **computed, not asked of you**: any blocking rubric verdict yields `request_changes`, otherwise the verdict is `approve`; a review of an elided (partial) diff yields `request_changes`. There is no third verdict: every rubric decides `pass` or `block` (code quality, which is advisory, decides `pass` or `flag`). 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`. 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.
 

.github/instructions/review.instructions.md

@@ -38,7 +38,7 @@ Each PR gets a short structured judgement covering:
   program behind it.
 - **Code quality**: 1 (clear AI slop) to 5 (mathlib-merge-ready).
 - **Significance**: one sentence saying what (or why not).
-- **Verdict**: `approve` / `request_changes` / `needs_discussion`.
+- **Verdict**: `approve` / `request_changes`.
 
 Then optionally a small list of specific, actionable findings — empty is
 fine and often correct.

.github/review-rubrics/faithfulness.md

@@ -29,15 +29,15 @@ Overclaiming usually lives in the *prose*, not the Lean: the theorem is honest,
 
 - `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.
+There is no third verdict; decide. A defensible but debatable formalization choice is a `pass` when the card discloses it, and a `block` naming the exact card wording that would make it honest when it does not.
 
 ## Output
 
 Return a single JSON object:
 
 ```json
 {
-  "verdict": "pass" | "block" | "discuss",
+  "verdict": "pass" | "block",
   "bottom_line": "<one sentence for the maintainer>",
   "proves_the_claim": "proves_it" | "weaker_than_claimed" | "mismatch" | "unverifiable",
   "claim_note": "<one sentence: what the main theorem actually says, especially where it is narrower than the card's prose>",

.github/review-rubrics/novelty.md

@@ -19,15 +19,15 @@ Not every overlap is duplication. A different proof of a known theorem, a sharpe
 
 - `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, Tau Ceti, 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.
+There is no third verdict; decide. Overlap that is arguably an extension is a `pass` when you can name what it adds, otherwise a `block`. Suspected prior art you cannot pin to a declaration is not a `block`; say what you searched.
 
 ## Output
 
 Return a single JSON object:
 
 ```json
 {
-  "verdict": "pass" | "block" | "discuss",
+  "verdict": "pass" | "block",
   "bottom_line": "<one sentence for the maintainer>",
   "already_formalized": "<the Mathlib, Tau Ceti, or pool declaration that already proves a headline — a bare declaration name and nothing else; EMPTY if none found or unchecked>",
   "novelty_note": "<one sentence: what is new here relative to the closest existing work, or what duplicates what>",

.github/review-rubrics/quality.md

@@ -24,18 +24,18 @@ 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."
+This dimension advises; it has no `block`. However bad the code, the worst you say is `flag`.
 
 - `pass` — competent or better; nothing a maintainer must weigh.
-- `discuss` — slop or debt bad enough that a human should look before merging.
+- `flag` — slop or debt worth fixing. It never blocks merging; the findings are the deliverable.
 
 ## Output
 
 Return a single JSON object:
 
 ```json
 {
-  "verdict": "pass" | "discuss",
+  "verdict": "pass" | "flag",
   "bottom_line": "<one sentence for the maintainer>",
   "code_quality": <int 1-5>,
   "findings": [

.github/review-rubrics/significance.md

@@ -32,15 +32,15 @@ A mixed PR can arrive with no new project in it — a Mathlib bump repairing eve
 
 - `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.
+There is no third verdict; decide. Real research-level content passes even when modest. Generated bulk passes when a stated verifier checks it and its maintenance cost is proportionate to the result; otherwise it is a `block`.
 
 ## Output
 
 Return a single JSON object:
 
 ```json
 {
-  "verdict": "pass" | "block" | "discuss",
+  "verdict": "pass" | "block",
   "bottom_line": "<one sentence for the maintainer>",
   "fit": "good_fit" | "borderline" | "not_a_fit" | "not_applicable",
   "level": "undergraduate" | "graduate" | "research",

.github/review-rubrics/sources.md

@@ -16,15 +16,15 @@ You usually cannot fetch the source. Judge from what the diff shows: the card's
 
 - `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.
+There is no third verdict; decide. An inconsistency you can point at but not settle from the diff is a `block` that names the discrepancy and the citation change that would resolve it.
 
 ## Output
 
 Return a single JSON object:
 
 ```json
 {
-  "verdict": "pass" | "block" | "discuss",
+  "verdict": "pass" | "block",
   "bottom_line": "<one sentence for the maintainer>",
   "source_match": "matches" | "mismatch" | "unverifiable" | "not_a_known_result",
   "findings": [

.github/workflows/stale.yml

@@ -2,29 +2,47 @@ name: Stale
 
 on:
   schedule:
-    - cron: '0 8 * * *'
+    - cron: '0 */6 * * *'
   workflow_dispatch:
 
 permissions:
   issues: write
   pull-requests: write
 
+concurrency:
+  group: stale
+  cancel-in-progress: false
+
 jobs:
-  stale:
+  stale-pull-requests:
+    permissions:
+      contents: read
+      issues: write
+      pull-requests: write
+    runs-on: ubuntu-latest
+    name: Label PRs stale at 7 days, close at 21 days
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
+        with:
+          persist-credentials: false
+      - name: Apply the age-based PR policy
+        env:
+          GH_TOKEN: ${{ github.token }}
+          REPOSITORY: ${{ github.repository }}
+        run: PYTHONPATH=python python3 -m lean_pool.stale_pull_requests --repository "$REPOSITORY"
+
+  stale-issues:
     runs-on: ubuntu-latest
+    name: Mark and close inactive issues
     steps:
-      - name: Mark and close stale issues and PRs
-        uses: actions/stale@b5d41d4e1d5dceea10e7104786b73624c18a190f
+      - uses: actions/stale@b5d41d4e1d5dceea10e7104786b73624c18a190f
         with:
-          days-before-pr-stale: 30
-          days-before-pr-close: 14
+          days-before-pr-stale: -1
+          days-before-pr-close: -1
+          remove-pr-stale-when-updated: false
           days-before-issue-stale: 90
           days-before-issue-close: 30
-          stale-pr-label: stale
           stale-issue-label: stale
-          exempt-pr-labels: pinned,roadmap,good-first-issue
           exempt-issue-labels: pinned,roadmap,good-first-issue
-          stale-pr-message: This PR has been inactive for 30 days and is marked stale.
-          close-pr-message: Closing this PR after another 14 days of inactivity.
           stale-issue-message: This issue has been inactive for 90 days and is marked stale.
           close-issue-message: Closing this issue after another 30 days of inactivity.

AGENTS.md

@@ -9,6 +9,7 @@ This file is a concatenation of README.md and CONTRIBUTING.md.
 [![Lean Action CI](https://github.com/LeanPool/lean-pool/actions/workflows/lean_action_ci.yml/badge.svg)](https://github.com/LeanPool/lean-pool/actions/workflows/lean_action_ci.yml)
 [![Documentation](https://img.shields.io/badge/docs-online-blue)](https://leanpool.github.io/lean-pool/)
 [![Exposition](https://img.shields.io/badge/exposition-online-8a4fff)](https://leanpool.github.io/lean-pool/exposition/)
+[![Source profile](https://img.shields.io/endpoint?url=https%3A%2F%2Fvilin97.github.io%2Flean-source-profiler%2Fpool%2Fbadge.json)](https://vilin97.github.io/lean-source-profiler/pool/)
 [![Zulip](https://img.shields.io/badge/Zulip-Lean_Pool-6492FE?logo=zulip&logoColor=white)](https://leanprover.zulipchat.com/#narrow/channel/619231-Lean-Pool)
 [![Semantic Search](https://img.shields.io/badge/semantic_search-Octo-2f80ed)](https://octo.axiomatic-ai.com/search?scopes=repo%3ALeanPool%2Flean-pool)
 [![License](https://img.shields.io/github/license/LeanPool/lean-pool)](LICENSE)
@@ -19,18 +20,17 @@ Lean Pool sits between [`mathlib`](https://github.com/leanprover-community/mathl
 
 Semantic search is also available via the [API](https://search.octo.axiomatic-ai.com/api/search).
 
+Explore compile costs in the [LeanPool source profile](https://vilin97.github.io/lean-source-profiler/pool/),
+from projects and files down to declarations and source lines.
+
 <!-- BEGIN STATS -->
-**289** formalization projects · **9,933,135** lines of Lean
+**319** formalization projects · **11,959,754** lines of Lean
 <!-- END STATS -->
 
 <sub>(stats above are refreshed automatically by the [generated-metadata workflow](.github/workflows/notice.yml) — edit [`python/lean_pool/stats.py`](python/lean_pool/stats.py), not the numbers)</sub>
 
 So far, projects have been added by hand: each is a suitable, permissively licensed (Apache-2.0 or MIT) Lean repository, bumped to the latest Lean and Mathlib, made to pass [CI](.github/workflows/lean_action_ci.yml) — it builds warning-free and clears Mathlib's linters, the style checker, and the repository quality gates (no `sorry`/`admit`, no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, no `unsafe`/`partial`, file headers, size limits) — and an [LLM review](.github/REVIEW_RULES.md) of fit and significance, then merged.
 
-LLM reviews use GPT-6-Astra at `xhigh` reasoning effort through a privately operated Codex worker, without paid OpenAI API requests or an API fallback. Reviews also show an estimated dollar cost at official Standard API token rates, labeled separately from Codex quota billing. See [review operations](python/review-operations.md) for deployment and diagnostics.
-
-Project PRs also receive an advisory Greptile review, configured in [`.greptile/`](.greptile/), for cross-file integration, reusable abstractions, completeness, maintainability, and measured cost. It supplements rather than replaces the independent LLM verdict.
-
 ### Getting started
 
 Requires Lean (via [`elan`](https://leanprover-community.github.io/install/), with the toolchain pinned in [`lean-toolchain`](lean-toolchain)) and Python 3.13+ with [`uv`](https://docs.astral.sh/uv/).
@@ -42,18 +42,14 @@ make setup    # pull Mathlib oleans, build the whole pool (~1.5h), install Pytho
 To work on a single project you don't need the whole pool built — see the
 [fast per-project build](CONTRIBUTING.md#dev-setup) in `CONTRIBUTING.md`.
 
-To regenerate the preserved Zeta5 numerical certificates, see the
-[certificate reproduction guide](scripts/zeta5-certificates/README.md).
-
-The [moving-sofa certificate recipe](python/lean_pool/sofa_certificates/README.md)
-regenerates its optimized certificate modules from pinned public inputs.
-
 ### Contributing
 
 See [`CONTRIBUTING.md`](CONTRIBUTING.md).
 
-The PR author or a maintainer can comment `/profile` to request an advisory
-compile-cost report. Failed or zero-phase timed runs show unavailable timing
+Every PR, including drafts, gets an advisory compile-cost comment, refreshed
+after pushes. PRs without added or modified Lean files get a no-files report.
+The PR author or a maintainer can also comment `/profile` to rerun it.
+Failed or zero-phase timed runs show unavailable timing
 and are excluded from totals; errors and any successfully measured heartbeat
 counts remain visible.
 
@@ -117,7 +113,7 @@ There are two paths:
 - **Propose a repo.** Open an issue with the GitHub URL and a maintainer can import it. Repos that Reservoir does not index can be added to [`candidates/manual.txt`](candidates/manual.txt).
 - **Open a content PR.** Add your project under `LeanPool/<YourProject>/`, register it in [`LeanPool/projects/<slug>.yaml`](LeanPool/projects/) — the card must declare `provenance` (`human`, `AI`, or `mix`; see below) — and regenerate the indexes with `lake exe mk_all`. Commit `LeanPool/<YourProject>/Imports.lean`, which publicly imports every project source. Lake discovers all pool modules automatically; keep `LeanPool.lean` unchanged. To use a project, import `LeanPool.<YourProject>.Imports`.
 
-Either way the result must pass CI (build, linters, and quality checks — see [Linting and testing](#linting-and-testing)) and an [LLM review](.github/REVIEW_RULES.md) of fit and significance. Accepted projects must be `sorry`-free, introduce no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, and avoid `unsafe`/`partial`. Each project card must also declare its **provenance** — who wrote the Lean proofs — as `human` (written by people), `AI` (mostly produced by an AI system), or `mix` (both contributed substantially). (Proof profiling via `/profile` is available but informational, not a gate: added files get an absolute profile, while modified files get a base→head compile-cost comparison — useful for checking that a refactor doesn't regress compile time.)
+Either way the result must pass CI (build, linters, and quality checks — see [Linting and testing](#linting-and-testing)) and an [LLM review](.github/REVIEW_RULES.md) of fit and significance. Accepted projects must be `sorry`-free, introduce no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, and avoid `unsafe`/`partial`. Each project card must also declare its **provenance** — who wrote the Lean proofs — as `human` (written by people), `AI` (mostly produced by an AI system), or `mix` (both contributed substantially). (Every PR gets an automatic proof-profile comment, refreshed after pushes and available on demand via `/profile`. It is informational, not a gate: added files get an absolute profile, while modified files get a base→head compile-cost comparison — useful for checking that a refactor doesn't regress compile time.)
 
 ## Dev setup
 
@@ -143,6 +139,7 @@ The whole-library checks (`lake exe runLinter LeanPool`, `lake exe lint-style Le
 - **Don't mix content and non-content changes.** A content PR may modify **only** `LeanPool/**/*.lean` and `LeanPool/projects/<slug>.yaml`. Infra / CI / tooling / doc changes may touch other files, but must not be bundled with content. This is enforced by [`content-pr-guard.yml`](.github/workflows/content-pr-guard.yml).
 - **Never change the checks or gates.** Do not modify `.github/workflows/`, `.github/CODE_QUALITY.md`, `python/lean_pool/quality.py`, `scripts/nolints-style.txt`, the `[leanOptions]`/lint settings in `lakefile.toml`, or any other CI step or linter config — and do not add a waiver of any kind (a `size-limit-ok` comment, a `nolints-style.txt` entry, `set_option linter.X false`, etc.) — unless explicitly asked. If a check fails, fix the code, not the check. This applies to everyone, and especially to AI agents.
 - **Branches.** `yourname/description` for solo work; `feature/`/`fix/` prefixes when shared. Open PRs early (draft + `WIP` is fine) and use `Closes #123` to link issues.
+- **Stale PRs.** A PR open for 7 days is labelled `stale`; one open for 21 days (and labelled for at least 7) is closed automatically by [`stale.yml`](.github/workflows/stale.yml). The `pinned` label exempts a PR.
 
 ## Linting and testing