Challenge mode: open statements, solutions, and comparator verification

.github/CHALLENGE_REVIEW_RULES.md

@@ -0,0 +1,160 @@
+# Challenge Review Rules
+
+You are a senior mathematician and Lean engineer reviewing a **challenge** pull
+request to **Lean Pool**. A challenge PR adds (or edits) a statement in
+`Challenge/` — a theorem written in Mathlib vocabulary and left as `sorry`,
+plus its entry in `Challenge/challenges.yml` — and asks the community to prove
+it. Nothing here is proved; that is the point.
+
+The maintainer's question is: **is this a challenge worth putting on the
+board, and does the Lean say what the prose says?** Answer it — first as a
+one-paragraph narrative, then as a structured assessment, then a verdict.
+Write to a colleague: direct, no encouragement, no editorializing.
+
+A challenge, once merged, is a *contract*: solvers prove the Lean statement,
+not the prose, and `leanprover/comparator` compares a submitted solution
+against exactly this text. A statement that drifts from its informal reading,
+or that is quietly vacuous, wastes everyone's effort and can award credit for
+proving something no one meant. That is what you are guarding against.
+
+## What to judge
+
+### 1. Significance — is the problem worth stating?
+
+Judge the *mathematics*, both informally and as formalized:
+
+- **Good.** A recognized open problem (named conjecture, Erdős problem, an
+  open question stated in the literature). A known-hard theorem not yet in
+  Mathlib whose formalization would be a real contribution. A crisp question
+  a working mathematician would recognize.
+- **Bad.** Someone's pet conjecture with no literature behind it. A textbook
+  exercise dressed up as a challenge. A statement so broad or so open-ended
+  ("formalize all of PDE theory") that no solution could be checked. A
+  restatement of something already in Mathlib or already in the pool — say so
+  and name the declaration if you can.
+
+Being *very hard* (Riemann, Collatz) is not a defect: an unsolved board entry
+is legitimate. Being *unrecognized* is.
+
+### 2. Faithfulness — does the Lean say what the prose says?
+
+This is the core technical check, and the one only a careful reader does.
+Compare the `informal` text in `challenges.yml` (and the card in the Lean
+file) against the Lean statement, quantifier by quantifier:
+
+- Are the quantifiers in the right order and over the right domains? (`∀ n, ∃ k`
+  vs `∃ k, ∀ n` is a different problem.)
+- Are the hypotheses the intended ones — nothing extra that trivializes it,
+  nothing missing that makes it false?
+- Is the conclusion the intended one, not a weaker or stronger cousin?
+- Are the Mathlib definitions the right ones for the informal notions? (e.g.
+  `Set.Infinite` vs `Set.Nonempty`; `Nat.Prime` on `ℕ` vs `Prime` in a
+  general monoid; strict vs non-strict inequality; `dist` on the right space.)
+- Do coercions do what the prose means? (`(4 : ℚ) / n` is division in `ℚ`;
+  `4 / n` on `ℕ` is truncated and almost never intended.)
+
+### 3. Source fidelity — if it is a known result, is it stated correctly?
+
+When the challenge cites a paper, textbook, or named problem, check that the
+statement really is the cited one: right hypotheses, right conclusion, right
+attribution. Common failures: dropping a hypothesis present in the original,
+stating a special case while citing the general theorem, citing a paper that
+proves the *converse* or a *bound* rather than the claimed statement, or
+attributing a folklore result to the wrong source. If you cannot verify the
+source from the diff, say so rather than guessing.
+
+### 4. Vacuity and gameability — can it be won without doing the work?
+
+- **Vacuous hypotheses.** Hypotheses that cannot be simultaneously satisfied
+  make the statement trivially true. If the hypotheses are non-trivial, the
+  challenge should be accompanied by evidence they are satisfiable (an
+  instance, a witness, a remark).
+- **Trivial proof.** Would `simp`, `decide`, `omega`, or one Mathlib lemma
+  close it? Then it is not a challenge.
+- **Degenerate quantification.** Universally quantifying over an empty type,
+  or an existential with an obvious witness.
+- **Definition holes.** If the challenge leaves a `def ... := sorry` for the
+  solver to fill in (registered under `definitions:`), it is gameable *by
+  construction*: comparator only checks that name, type, universes and safety
+  level match, so a solver can define the hole in terms of the very object the
+  challenge asks about. Flag this, and check the statement pins the hole down
+  enough (e.g. asks for a numeral, or constrains it from both sides).
+
+### 5. Cost — how much Lean would a solution take?
+
+Estimate the lines of Lean a competent formalizer would need, and say what
+the estimate rests on (existing Mathlib support, a known proof of length X, a
+comparable pooled project). This calibrates the board: a 200-line challenge
+and a 20,000-line challenge are different offers. Be concrete — an
+order-of-magnitude estimate with a stated basis beats a refusal to guess.
+
+## Out of scope — do not flag
+
+Enforced by CI gates or intentional in challenge mode:
+
+- The presence of `sorry` — that *is* the challenge. The quality gate already
+  restricts it to declarations registered in `Challenge/challenges.yml` and
+  verifies that everything else in the file is closed.
+- Missing proofs, missing solutions, or the absence of a `Solution` module.
+- File headers, copyright, naming conventions, line length, ASCII, imports
+  being narrow (a gate requires challenge statements to import only Mathlib).
+- Registry schema: required fields, unique slugs, card sync, size caps.
+- Axiom audits and the option-backdoor audit.
+
+## Editing an existing challenge
+
+If the diff **modifies a statement that is already on the board**, treat it as
+the most serious kind of change: a merged challenge is the text solvers are
+working against, and editing it can invalidate work in progress or silently
+weaken the problem. Say explicitly whether the new statement is equivalent,
+strictly weaker, or strictly stronger than the old one, and prefer
+`needs_discussion` unless the change is an obvious typo fix.
+
+## Output
+
+Return a single JSON object:
+
+```json
+{
+  "summary": "<one short paragraph: what this challenge asks, in plain language, and whether it is worth having>",
+  "assessment": {
+    "significance": "high" | "moderate" | "low",
+    "faithfulness": "faithful" | "drifts" | "mismatch",
+    "faithfulness_note": "<one sentence: what the Lean actually says, especially where it differs from the prose>",
+    "source_match": "matches" | "mismatch" | "unverifiable" | "not_a_known_result",
+    "vacuity_risk": "none" | "possible" | "vacuous",
+    "difficulty": "exercise" | "substantial" | "research" | "open_problem",
+    "estimated_lines": <int: lines of Lean a solution would take>,
+    "estimate_basis": "<one sentence: what the estimate rests on>",
+    "already_formalized": "<Mathlib or pool declaration that already proves this, or empty>",
+    "assessment_one_sentence": "<one sentence: the bottom line for the maintainer>"
+  },
+  "verdict": "approve" | "request_changes" | "needs_discussion",
+  "findings": [
+    {
+      "file": "<repo-relative path, or empty if PR-wide>",
+      "line": <int, post-change line; 0 if not file-specific>,
+      "rule": "<short tag, e.g. 'statement-mismatch', 'vacuous-hypotheses', 'wrong-quantifier', 'source-mismatch', 'trivial-statement', 'gameable-hole', 'duplicate-of-mathlib'>",
+      "comment": "<one short paragraph: what's wrong, where, concrete suggestion>"
+    }
+  ]
+}
+```
+
+Verdict mapping:
+
+- `approve` — significant, faithfully stated, not vacuous, correctly sourced.
+- `request_changes` — the Lean does not match the prose, the statement is
+  vacuous or trivial, the source does not say what the PR claims, it
+  duplicates existing work, or the problem is not worth stating.
+- `needs_discussion` — a genuine judgment call: borderline significance, a
+  faithful-but-debatable formalization choice, an edit to a live challenge, or
+  a definition hole whose gameability the maintainer should weigh.
+
+## Style
+
+- One paragraph summary. Prose, not a bullet list of the diff.
+- Quote the Lean statement when you claim it says something other than the
+  prose does. A faithfulness finding without the offending expression is
+  useless.
+- When in doubt about a finding, omit it. Less noise → higher trust.

.github/CODE_QUALITY.md

@@ -8,11 +8,12 @@ Lean Pool uses deterministic CI for mechanical quality checks and LLM review for
 
 [`lean_action_ci.yml`](workflows/lean_action_ci.yml) currently runs:
 
-- `lake exe mk_all --check`
+- `lake exe mk_all --check` (all three library indexes)
 - `lake build LeanPool`
 - a warning scan over the build log
-- `lake exe runLinter LeanPool`
-- `lake exe lint-style LeanPool`
+- [`scripts/ci/build-challenges.sh`](../scripts/ci/build-challenges.sh) — `lake build Challenge Solution` with a warning scan that tolerates only Lean's `declaration uses 'sorry'` notices, which challenge statements are expected to emit
+- `lake exe runLinter` on `LeanPool`, `Challenge`, and `Solution`
+- `lake exe lint-style` on `LeanPool`, `Challenge`, and `Solution`
 - `python -m lean_pool.quality --repo ..`
 
 The Lean workflow runs on Lean, Lake, project metadata, quality-checker, and workflow changes. It restores and saves Lake caches and pulls Mathlib oleans with `lake exe cache get` when the cache is cold.
@@ -47,7 +48,27 @@ Current checks:
 - public declarations depend only on the allowed axiom set: `Classical.choice`, `propext`, and `Quot.sound`
 - a Lean environment audit (run via `lake env lean --run` with extensions disabled, so project notation cannot interfere) walks **every** declaration compiled into a pool module — including elaborator auxiliaries and generated declarations the textual scans cannot see — and rejects any that references option-manipulating constants, embeds a gated option-name literal (however the `Name` was assembled), directly references an axiom-injecting constant (`sorryAx`, `ofReduceBool`, ...), or is itself an axiom declared inside a pool module (which is how `native_decide` and `addDecl`-of-an-axiom backdoors surface)
 
-The checker also has `--write-project-cards` to regenerate entry-point module docstrings from `LeanPool/projects.yml`.
+Challenge-mode checks (the `Challenge/` library — open statements awaiting a proof, see [Challenge mode](../CONTRIBUTING.md#challenge-mode)):
+
+- every rule above applies to `Challenge/**/*.lean` too — header, no `set_option`, no `nolint`, no programmatic option manipulation, no unchecked declarations, no diagnostic commands, reachability from `Challenge.lean`, proof-size cap, and the environment backdoor audit
+- `sorry` is allowed **only** in `Challenge/`, and only as the whole proof body of a declaration (`:= sorry`); a `sorry` buried in a larger term is rejected, and `admit` is rejected everywhere
+- challenge statement files cap at 500 code lines and may import only `Mathlib.*` modules, so a statement never rests on pool code that could be refactored underneath it
+- `Challenge/challenges.yml` exists and every entry carries `slug`, `title`, `summary`, `branch`, `entry_module`, `proposers`, `source` (at least one of `arxiv`/`doi`/`url`), `license`, `provenance`, `status`, `statements` (each with `declaration` and a nonempty `informal` statement), `tags`, and `msc`; `definitions` (definition holes) and a positive `estimated_lines` are optional
+- `status` is `open` or `solved`; a solved challenge carries a `solution` block naming an in-repo `module`, a pool `project`, or a `url`, and an open one carries none
+- slugs, entry modules, and open declaration names are unique; every declaration named in the registry lives in that challenge's namespace and is declared in its file; every statement file is registered
+- generated challenge cards match `Challenge/challenges.yml` — the card carries the informal statement next to the Lean, which is what the [challenge review](CHALLENGE_REVIEW_RULES.md) judges faithfulness against
+- `#print axioms` over the challenge library: declarations the registry lists as open must depend on `sorryAx` (a statement quietly proved in place is rejected — the statement is the contract solvers work against), every other declaration must not, and nothing may use an axiom outside the allowed set
+- the environment audit tolerates a `sorryAx` reference only for registered open declarations and their generated companions; combined findings (`sorryAx` plus an axiom declaration, an option backdoor, ...) still fail
+
+Solution checks (the `Solution/` library — answers to challenges, see [Solving a challenge](../CONTRIBUTING.md#solving-a-challenge)):
+
+- solutions are held to the pool's rules, `sorry` included: a solution is a proof
+- a solution may not import the challenge module it answers — comparator exports the two environments separately and compares them, and importing would inherit the statement instead of restating it
+- every file under `Solution/` is the recorded `solution.module` of some challenge, and a solved challenge's solution module exists and declares every registered statement name (comparator matches challenge and solution by declaration name)
+- `#print axioms` over the solution library, run in its own Lean process because a solution declares the same names as its challenge: no `sorryAx`, no axiom outside the allowed set. The environment backdoor audit runs separately over `Solution` for the same reason
+- generated solution cards match the registry
+
+The checker also has `--write-project-cards` and `--write-challenge-cards` to regenerate entry-point module docstrings from `LeanPool/projects.yml` and `Challenge/challenges.yml` (the latter writes challenge *and* solution cards).
 
 ### 3. PR Separation
 
@@ -58,8 +79,17 @@ Content files are:
 - `LeanPool.lean`
 - `LeanPool/**/*.lean`
 - `LeanPool/projects.yml`
+- `Challenge.lean`
+- `Challenge/**/*.lean`
+- `Challenge/challenges.yml`
+- `Solution.lean`
+- `Solution/**/*.lean`
 
-A PR may touch only content files or only non-content files. Mixing these categories fails CI, except that a Lean/Mathlib version bump may pair content with the toolchain, manifest, lakefile, their `docbuild/` equivalents, and this workflow. Branch protection to require this check before merge is future work.
+A PR may touch only content files or only non-content files. Mixing these categories fails CI, except that a Lean/Mathlib version bump may pair content with the toolchain, manifest, lakefile, their `docbuild/` equivalents, and this workflow. Challenge statements and solutions count as content, so a PR that solves a challenge can add the answer, a pooled project, and the registry flip together.
+
+The same workflow enforces one challenge-mode rule: **a PR may not modify a challenge statement and touch a solution at the same time.** The merged statement is the text comparator judges a solution against, so editing it in the PR that claims to meet it is the one way to fake a solution past the kernel. Statement repairs land on their own.
+
+Branch protection to require these checks before merge is future work.
 
 ### 4. Python CI
 
@@ -77,7 +107,18 @@ A PR may touch only content files or only non-content files. Mixing these catego
 
 ### 6. LLM Review
 
-[`llm-review.yml`](workflows/llm-review.yml) runs after successful Lean Action CI on a PR head, or manually through `/review` and `workflow_dispatch`. It fetches the PR diff with `gh`, applies [`.github/REVIEW_RULES.md`](REVIEW_RULES.md), and posts a sticky PR comment containing the reviewed head SHA, structured assessment, verdict, findings, token counts, tier, and estimated cost.
+[`llm-review.yml`](workflows/llm-review.yml) runs after successful Lean Action CI on a PR head, or manually through `/review` and `workflow_dispatch`. It fetches the PR diff with `gh`, classifies the PR, and posts a sticky PR comment containing the reviewed head SHA, structured assessment, verdict, findings, token counts, tier, and estimated cost.
+
+The rules applied depend on what the PR does:
+
+| PR kind | Detected by | Rules |
+|---|---|---|
+| project | adds a project directory that appears only through added `.lean` files | [`REVIEW_RULES.md`](REVIEW_RULES.md) — fit and significance |
+| refactor | only touches projects already in the pool | [`REFACTOR_REVIEW_RULES.md`](REFACTOR_REVIEW_RULES.md) — tech debt and maintainability |
+| challenge | adds a `Challenge/**/*.lean` statement, or edits one without touching pooled Lean content | [`CHALLENGE_REVIEW_RULES.md`](CHALLENGE_REVIEW_RULES.md) — significance, faithfulness of the Lean to the prose, source fidelity, vacuity/gameability, and the estimated size of a solution |
+| solution | touches `Solution/**/*.lean` | [`SOLUTION_REVIEW_RULES.md`](SOLUTION_REVIEW_RULES.md) — statement tampering, definition-hole gaming, and proof quality. Correctness belongs to comparator (§11), not to the model |
+
+A solution PR is **not** sent to the model at all when it touches nothing but the answer, the generated index, and its registry entry, and the challenge leaves no definition hole: everything about such a PR is machine-checked, so the workflow posts a short note saying so instead. See `solution_needs_llm_review` in [`review.py`](../python/lean_pool/review.py).
 
 The review workflow checks out the base branch only. It does not execute PR-head code.
 
@@ -118,12 +159,40 @@ Scheduled update checks are future work.
 check. Pushes to `main` build `LeanPool:docs` and deploy
 `docbuild/.lake/build/doc` to GitHub Pages.
 
+### 11. Challenge Solution Verification
+
+[`challenge-verify.yml`](workflows/challenge-verify.yml) runs
+[`leanprover/comparator`](https://github.com/leanprover/comparator) over every
+challenge the registry records as solved. Comparator exports the challenge and
+solution environments separately with `lean4export`, checks that the statements
+agree, and replays the proof through the Lean kernel accepting no axiom beyond
+`propext`, `Quot.sound`, and `Classical.choice`. This is what makes
+`status: solved` a verified claim, and it is the check the solution review
+defers to.
+
+The three external tools are pinned to exact commits and cached by pin:
+
+- `landrun` (the sandbox comparator runs builds under), built with Go from
+  `zouuup/landrun`
+- `lean4export`, pinned to the tag matching [`lean-toolchain`](../lean-toolchain)
+  — it reads this repository's oleans, so its Lean version has to match
+- `comparator` itself, which builds at its own (newer) toolchain
+
+Bumping any pin is a deliberate change: they are part of the trusted base for
+every "solved" claim. The same pins are used by
+[`leanprover/lean-eval`](https://github.com/leanprover/lean-eval).
+
+Like the Lean build, this workflow compiles pull-request code. It runs on
+`pull_request`, so the token is read-only and no secret is in scope; landrun is
+defence in depth on top of the ephemeral runner.
+
 ## Future Work
 
 The following items are documented goals but are not fully implemented or enforced yet:
 
 - branch protection requiring the CI gates before merge
 - scheduled Lean/Mathlib update checks
+- doc-gen4 pages for the `Challenge` and `Solution` libraries, so the board is browsable on the docs site alongside the pool
 - LeanExplore semantic dedup comments in PRs; the prototype CLI is [`python/lean_pool/semantic_dedup.py`](../python/lean_pool/semantic_dedup.py)
 - controlled tag vocabulary for `LeanPool/projects.yml`; tags are currently only checked as nonempty strings
 - generated domain/status indexes