[Vilin97]

Delete the retired challenge board, its registry, and the standalone solution library after #575 disables challenge infrastructure.

This removes six statement modules, three solution modules, their generated root indexes, and Challenge/challenges.yml. The completed projects under LeanPool/ remain unchanged. Repository history preserves the retired statements and solutions.

Depends on #575 and targets its branch so the deletion is reviewed separately from infrastructure changes. Land #575 first, then retarget this PR to main; leave both PRs unmerged until review. The needs-manual-rebase label keeps the automatic updater from merging main into this stacked branch independently of its parent; update it from #575 until the stack is landed.

Validation:

• lake exe mk_all --check passes after deletion without recreating either retired root.
• Full Python suite: 525 passed, 2 opt-in integration skips requiring a prebuilt Mathlib workspace; Ruff, actionlint, and whitespace checks.
• Hosted Python CI and documentation preflight pass on the combined branch. These checks were dispatched explicitly because the normal build workflows target main rather than the stacked base branch.
• Source/import inventory confirms no remaining project or infrastructure dependency on the deleted libraries.
• The infrastructure PR's full static quality scan passes; the pooled sources and project registry are identical here.

Full Lean builds and Lean-backed audits are covered by hosted CI, 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.

[Low risk] Removes retired challenge and solution files.

This PR appears safe to merge after its parent PR lands.

Findings

1.  Mixed PR changes ▶

Summary

This PR removes the retired challenge statements, standalone solutions, generated root indexes, and challenge registry after the parent PR removes their infrastructure. The completed LeanPool/ projects remain outside this PR's diff.

_{Reviews (5) · Last reviewed commit: "Merge branch 'codex/remove-challenge-inf..."}

[Vilin97]

Reviewed 70c99998385bbcce1077f5ff87273a2a891165aa against stacked base b0bf82ca8a7ec5e82bed8bd8845c5cc32b4de023 (#575). Changes requested before integration. The complete twelve-file delta removes six registered statements, three solutions, two generated roots and the registry: 1,269 deleted lines, with no pooled source, project-card or additional gate change relative to that base.

The two standalone completed solutions deserve an explicit retention decision. Solution/BudgetedSubmodular.lean contains the 342-line modified-greedy development; Solution/TestingByBetting.lean contains the 187-line wealth/supermartingale/Ville development. Neither is migrated into a supported pooled library by this diff. Preserve these completed proofs in an appropriately attributed library before deleting the feature bridges, or make their deliberate removal explicit in the approved retirement scope. The Odlyzko solution is a thin bridge to the retained pooled proof; that underlying development remains present. This review does not claim the two other results are absent everywhere in Mathlib or the repository.

The proposed #575-first transition currently removes verification while retaining three solved registry claims until this PR lands. Resolve the P1 transition finding and establish explicit human authorization for the protected gate-retirement/parser scope in #575 before integrating the stack. The current goal/model authorization does not supply that separate exception to AGENTS.md.

Exact combined-head Python CI 37041424923, documentation preflight 37041421110 and separation passed. No Lean Action CI run or protected full Build project verdict is present for this combined head at this review. After any approved prerequisite and retargeting, recheck the actual latest main/head, deletion inventory, full required checks and conversations. Earlier or prerequisite runs do not substitute for those successor checks.

This author-account COMMENTED review records the requested-changes disposition under the continuing GPT-6.1-Sol/Ultra review. No deletion, gate edit, local build, retarget or merge was performed.

[greptile-apps]

Mixed PR changes

This import adds the OrderClosures project to a PR that also deletes non-content files under Challenge/ and Solution/. The repository requires content and non-content changes in separate PRs, and its PR separation guard rejects this combination. Move the project addition to a content-only PR so the retired-library removal can pass the guard.

File Used: CONTRIBUTING.md (source)

Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!

[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]

Reviewed cefdbd57c9173a3ace93adbb947aac8f58b0a68b relative to its #575 stacked base. The twelve-file diff deletes six live challenge statements, all three solution bridges, both indexes and the registry; it does not add a proof or change any pooled project. The previous mixed-content finding was on an older topology and does not apply to this content-only head.

The remaining human decision is whether Lean Pool deliberately retires these accepted contracts and discards the standalone completed BudgetedSubmodular and TestingByBetting developments, or preserves those proofs in supported, attributed pooled modules before deletion. The Odlyzko bridge's underlying pooled proof remains. Current CONTRIBUTING policy promises immutable merged challenge statements; the PR description is evidence of a proposal, not authorization to override that policy. This is a policy/retention choice that automation cannot infer from CI. Please explicitly settle the retirement/retention scope. The separate #575 verification-gap change request must also be resolved before integrating the stack.

Disposition: needs-maintainer solely for that policy and proof-retention decision. A merge would decide it implicitly; a code change request or closure would choose one of the policy outcomes without authority. Behind-main status, the stacked base and pending integration are not the reason for this label.