Challenge mode: open statements, solutions, and comparator verification

[Vilin97]

The other half of the pool: Challenge/ holds open statements — theorems written in Mathlib vocabulary and left as sorry — and Solution/ holds answers to them. Both libraries ship empty here; the first challenges land in the stacked PR that follows, so the machinery gets exercised by a real content PR.

The board

sorry is allowed only in Challenge/, and only as the whole proof body of a declaration registered in Challenge/challenges.yml. The gates keep the board honest:

• every other declaration in a statement file is closed — checked with #print axioms, so scaffolding can't hide behind an open statement;
• a registered statement really is open (a statement quietly proved in place is rejected — it is the contract solvers work against);
• statements import only Mathlib.*, so reading a challenge never means auditing pool code;
• the generated card, which carries the informal statement the Lean is judged against, matches the registry;
• headers, set_option, axioms, the option-backdoor audit and size caps apply exactly as they do to pooled projects.

Solutions

A solution restates its challenge's statement under the same name and proves it, and may not import the challenge module: leanprover/comparator exports the two environments separately and checks that the statements agree, which is what makes the verdict independent of the statement file.

challenge-verify.yml runs comparator over every solved challenge, with landrun, lean4export (pinned to the tag matching our toolchain) and comparator pinned to exact commits — the same pins leanprover/lean-eval uses. Locally, make comparator + make verify-challenge C=<slug>.

Verified end to end on a throwaway fixture before this PR was split out: a correct solution gives Your solution is okay!; a weakened statement gives Challenge and solution theorem statement do not match; a solution still using sorry gives Illegal axiom detected: 'sorryAx'.

Review

classify_pr now recognizes four kinds — project, refactor, challenge, solution:

kind	judged on
challenge	significance, faithfulness of the Lean to the prose, source fidelity, vacuity/gameability, estimated size of a solution
solution	statement tampering, definition-hole gaming, proof quality — correctness belongs to the kernel

A solution PR gets no model call at all when it touches nothing but the answer, the generated index, and its registry entry, and the challenge left no definition hole: everything about it is machine-checked, so the workflow posts a short note saying so.

The PR guard treats statements and solutions as content, and rejects a PR that edits a statement and a solution together — that is the one way to fake a solution past comparator. Challenge.lean and Solution.lean are neutral: generated indexes with no mathematics in them.

Checks run locally

lake exe mk_all --check, lake build Challenge Solution, runLinter/lint-style on both new libraries, the quality checker (static + the Lean-backed axiom audits), 238 pytest tests, ruff, actionlint, shellcheck.

🤖 Generated with Claude Code

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.

[greptile-apps]

Greptile Summary

This PR introduces challenge mode — the "other half of the pool" — shipping two new Lean libraries (Challenge/ for open statements, Solution/ for answers), the full Python machinery to gate and review them, and a new CI workflow that runs leanprover/comparator over every solved challenge pinned to exact tool commits.

• Quality gates: quality.py is extended with whole-body-sorry enforcement, Mathlib-only import checks, a two-pass environment audit (Challenge + LeanPool together; Solution separately to avoid name collisions), and the #print axioms open-declaration audit that now correctly requires sorryAx to be present for registered open statements and absent for everything else.
• PR classification: review.py gains \"challenge\" and \"solution\" PR kinds; solution PRs with nothing beyond the answer and registry entry skip the model call entirely.
• Verification pipeline: challenge-verify.yml builds comparator/lean4export/landrun from pinned commits, caches them keyed on toolchain hash, and replays every solved challenge; verify-solution.sh drives the same flow locally.

Confidence Score: 5/5

Safe to merge — all correctness-critical gates (axiom audit, sorry policy, import restrictions, comparator verification) are implemented correctly and the previously identified open-declaration proof-without-sorry gap has been closed.

The axiom-audit fix from the prior review thread is in place: _axiom_errors now checks if is_open and SORRY_AXIOM not in axioms before inspecting extra axioms, so a challenge proved classically is caught. The two-pass environment audit correctly separates Challenge + LeanPool from Solution to avoid name collisions. Comparator tool pins, caching, and sandbox logic look sound. The only finding is a shell variable named config instead of configuration in verify-solution.sh.

Files Needing Attention: No files require special attention.

Important Files Changed

Filename	Overview
python/lean_pool/challenge.py	New module: challenge registry schema, card generation, and comparator JSON configuration. Well-structured with clear separation between domain logic and enforcement gates.
python/lean_pool/quality.py	Extends quality gates to Challenge and Solution libraries: sorry-whole-body-only textual check, Mathlib-only import enforcement, open-declaration axiom audit with correct sorryAx presence/absence checking, and two-pass environment audit to avoid name collisions between Challenge and Solution.
python/lean_pool/review.py	Adds challenge/solution PR kinds to the classifier and review pipeline; introduces solution_needs_llm_review skip logic and four-mode rendering infrastructure.
.github/workflows/challenge-verify.yml	New workflow: builds comparator, lean4export, and landrun at pinned commits, then replays every solved challenge through the Lean kernel. Tools are cached by commit hash + toolchain.
.github/workflows/content-pr-guard.yml	Extends PR guard to cover Challenge/Solution content files and adds the mixed-statement-and-solution rejection; the unreachable success-message branch (line 157) noted in a prior outside-diff comment remains.
scripts/challenge/verify-solution.sh	New script: drives comparator locally and in CI with landrun sandboxing. Minor naming convention violation: shell variable config should be configuration.
python/lean_pool/stats.py	Adds open_challenges counter to Stats; render_stats omits the challenge line when the board is empty.

Sequence Diagram

sequenceDiagram
    participant PR as Solution PR
    participant Guard as content-pr-guard.yml
    participant LeanCI as lean_action_ci.yml
    participant Verify as challenge-verify.yml
    participant Review as LLM review

    PR->>Guard: push / PR opened
    Guard->>Guard: reject if Challenge statement modified + Solution added
    Guard->>Guard: reject if content + non-content mixed

    PR->>LeanCI: quality checks
    LeanCI->>LeanCI: sorry/axiom audit (Challenge library)
    LeanCI->>LeanCI: sorry forbidden in Solution
    LeanCI->>LeanCI: solution must not import Challenge

    PR->>Verify: challenge-verify.yml
    Verify->>Verify: lake build Challenge
    Verify->>Verify: lean4export (challenge env)
    Verify->>Verify: comparator: statements match?
    Verify->>Verify: kernel replay: no sorryAx?

    PR->>Review: classify_pr
    Review->>Review: solution_needs_llm_review?
    alt nothing beyond answer + registry
        Review-->>PR: skip comment (no model call)
    else definition hole or extra files
        Review->>Review: SOLUTION_REVIEW_RULES.md
        Review-->>PR: LLM comment
    end

Loading

_{Reviews (2): Last reviewed commit: "Close the axiom-gate hole a challenge pr..." | Re-trigger Greptile}

[github-actions]

🤖 LLM review (gpt-5.5)

Reviewed head: 211141c9707af9fa7a801398a2b497bbc81bd514

Verdict: 🛑 request_changes

This PR adds a Challenge/Solution mode around open Lean statements, generated cards, registry validation, LLM review routing, and comparator-based verification. The direction is repository infrastructure rather than a mathematical project, but the implementation has blocking correctness issues in the review skip logic and the solution audit boundary, and the docs workflow appears to call a doc target not added to the docbuild workspace.

Aspect	Value
Fit	🟡 borderline
Level	undergraduate
Branch	repository infrastructure
Mode	mixed
Obscure problem	no
Code quality	3 / 5

The contribution is a challenge-board and verified-solution workflow, not a formalized mathematical theorem.

Findings (3)

• definition-hole-skip — python/lean_pool/review.py:522
solution_needs_llm_review reads Challenge/challenges.yml from the base checkout, but the review workflow does not apply the PR diff. A normal solution PR flips the registry to add solution.module only in the PR, so this function will usually see no solution module and will skip the model even when the base challenge has definitions:. Either inspect the PR-head registry/diff, or make definition-hole detection use the base challenge entry independently of the PR's new solution block.
• audit-scope — python/lean_pool/quality.py:786
_run_option_audit always passes _open_declarations(root) into _parse_option_audit_output, including for the separate Solution audit. Since solutions deliberately declare the same fully qualified theorem names as challenges, this suppresses pure sorryAx environment-audit findings for solution declarations with registered challenge names. Pass the tolerated open-declaration set only for the Challenge audit and an empty set for Solution.
• docs-build — .github/workflows/docs.yml:164
  The docs workflow now runs lake build LeanPool:docs Challenge:docs inside docbuild, but the diff does not add a Challenge library to the docbuild Lake workspace. Unless that target already exists on base, this makes the docs job fail; add the corresponding docbuild library configuration or do not request Challenge:docs yet.

---

Tokens: 55,839 in / 6,229 out · Tier: flex · Cost: $0.2330
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.