[Vilin97]

Challenge mode is being retired because maintaining its separate statement, solution, and verification pipeline has become too costly. Lean Pool will accept completed projects through the existing project gates.

This removes challenge libraries from Lake and default targets; comparator tooling and verification CI; challenge/solution build, lint, profiling, documentation and cache integration; registry/card generation; review routing and rubrics; statistics; and obsolete tests. README, contributor guidance, generated agent instructions, and quality documentation describe the remaining project workflow. Project lint, axiom, option-backdoor, size, and content-separation checks remain enforced, with no proof-hole exceptions.

The multiline axiom parser fix from #564 is retained with project-quality regression tests, including wrapped forbidden axioms. #564 and challenge issue #563 have been closed as part of retiring the feature.

This is the infrastructure half of a two-PR stack. The follow-up #576 deletes the retired statement/solution Lean files, root indexes, and registry. Keeping those deletions separate respects the existing content/infrastructure separation gate. Review and land this PR before that follow-up; neither PR should be merged automatically.

Validation:

• Full Python suite: 525 passed, 2 opt-in integration skips requiring a prebuilt Mathlib workspace, including proof-hole rejection, wrapped axiom output, and default index-generation regression coverage (a shell-local nproc implementation supplies CPU count on macOS; no repository change or test waiver).
• Ruff lint and formatting, actionlint, and whitespace checks. Hosted Python CI, workflow lint, and documentation preflight pass on the current head.
• lake exe mk_all --check and full-repository static quality check.
• PR separation guard exercised for content-only, infrastructure-only, valid version-bump, and rejected mixed-scope changes.

No pooled project source or dependency pin changes. Full Lean builds and Lean-backed repository audits are left to hosted CI; they are not claimed as locally verified.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Medium risk] Removes challenge and solution infrastructure from the repository.

This PR does not appear safe to merge before the retained challenge and solution content is removed or its verification remains in place.

Findings

1.  Retained solutions lose verification ▶

Summary

This PR removes challenge-mode build, verification, review, quality-check, and documentation infrastructure while retaining the completed-project gates. PR #576 is intended to remove the remaining challenge and solution content afterward.

_{Reviews (4) · Last reviewed commit: "Merge main and refresh project statistic..."}

[greptile-apps]

Retained solutions lose verification

This removes Challenge and Solution from the default Lake targets, but this PR leaves their Lean files and three registry entries marked solved in place. The CI build no longer compiles those files, and the comparator workflow that checked each solution against its statement is also removed. Because this PR is meant to land before #576, a changed solution or solved claim can pass the remaining gates without being verified. Keep those checks until the content is removed, or retire the content and claims together.

[Vilin97]

Reviewed b0bf82ca8a7ec5e82bed8bd8845c5cc32b4de023 against main 16ac1e76587e01548c71d8ed96e298e87ecfd4ed. Changes requested before integration. This review covers the complete 37-file retirement delta and preserves the current project-only proof and trust safeguards; it does not approve a gate-policy change.

1. Resolve the verification gap in the proposed merge order. Removing the Challenge/Solution Lake targets, build/lint/comparator steps and registry audit while retaining six statements, three solutions and three solved registry claims leaves the intermediate main commit without verification for that content. The existing Greptile P1 is valid. Landing #576 later does not validate that intermediate state. Keep verification for all retained claims until they are retired, or provide a reviewed transition that leaves no integrated commit with unverified retained claims. Project CI success alone does not resolve this finding.
2. Establish the explicit protected scope. AGENTS.md requires an explicit request before changing checks or gates. This PR also includes the wrapped-axiom parser change from closed, unmerged #564. The current import-merge and GPT-6.1-Sol/Ultra directions do not authorize that separate parser change or challenge-gate retirement. The inspected PR and coordination evidence establishes the proposal, but no distinct direct human scope authorization. That condition must be resolved before any protected integration; closing #564 supplies no authorization.
3. Account for the content successor and its checks. #576 removes the twelve remaining content paths, including two standalone completed proofs with no migration into LeanPool. Review that deliberate source removal as part of the retirement decision. After any approved base/main transition, both affected integration heads need their normal protected checks and resolved conversations. The current #576 combined head has Python/docs/separation success but no exact-head full Lean Build project verdict.

The remaining project gates retain the standard allowed axioms, proof-hole rejection, backdoor audit and size limits. I found no further concrete retirement-wiring defect in this bounded review; ProjectIndexes registration is preserved, and pooled source, project registry, dependency manifest and toolchain are unchanged. Full Lean run 37041312875 is still pending at this review, so no terminal build/quality verdict is claimed.

This author-account COMMENTED review records a requested-changes source/policy disposition under the continuing GPT-6.1-Sol/Ultra review; no source or gate edit, local build, or merge was performed.

[github-actions]

Auto-rebase stopped: this PR conflicts with main outside the two
mechanically resolvable files (LeanPool.lean, LeanPool/projects.yml),
so the overlap needs a human. Remove the needs-manual-rebase label once
resolved to re-enable automatic updates.

[Vilin97]

Changes requested by automated review

Reviewed d2ba554bad2252d6b51710c6b6e8bef7744b3cc6, including the complete 37-file infrastructure delta, tests, current green Python/workflow/Lean CI, and the unresolved verification-gap thread. The project-only wrapped-axiom parser change is covered by regression tests; the green build does not establish safety of the retirement transition.

The proposed #575-first order removes Challenge/Solution targets and comparator/build/lint/registry validation while leaving six registered statements, three solution modules, and three solved registry claims in main until #576 lands. This is the still-valid P1 finding at https://github.com/Vilin97/lean-pool/pull/575#discussion_r4168218479. Keep verification for every retained claim through the transition, or design a reviewed transition with no integrated commit containing unverified retained claims. Retiring the live challenge contracts also needs an explicit policy decision; this autonomous review does not authorize weakening live gates.

Disposition: changes requested. The remaining defect is concrete and author-actionable, so it is not a needs-maintainer label. No gates or policy were changed by this review.