Keep the challenge card free of lifecycle, so a challenge can be solved

[Vilin97]

No description provided.

[github-actions]

Proof profile (new / modified Lean files)

Statement changes

✅ No statements changed — all 2 tracked declarations across 2 modified files kept their type; only proofs / definition bodies changed.

Statements are compared textually against the merge base (comments and whitespace ignored; by proof terms embedded in a type are treated as proof-irrelevant), the same method as physlib's /check-golf. Anonymous instances and examples are not tracked.

Compile cost of modified files — base → head

Heartbeats: 6 → 6 (+0, +0.0%). Declarations: 2 → 2.

Per-file wall sum: 8.6 s → 8.1 s (-5.5%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal.

Files: 2 compared — 0 cheaper, 0 costlier, 2 within noise (threshold: |Δ heartbeats| ≥ 1,000 and ≥ 1%).

Both sides are elaborated against the merge-base build of the pool — sound when only proofs and definition bodies change; a file whose statements changed may fail there and is flagged ⚠. Heartbeats come from Mathlib's linter.countHeartbeats, in maxHeartbeats units. Δ lines counts added/deleted lines from this PR diff.

File	Δ lines	HB base	HB head	Δ HB	Δ HB %	Wall base (s)	Wall head (s)
Challenge/Mazur.lean	+0/-1	3	3	+0	+0.0%	4.19	3.95
Challenge/Odlyzko.lean	+0/-1	3	3	+0	+0.0%	4.38	4.15
Total	+0/-2	6	6	+0	+0.0%	8.6	8.1

Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.

[greptile-apps]

Greptile Summary

This PR fixes a deadlock that made solving any challenge impossible: the generated challenge card previously included Status: open, which the card-check gate would require to be updated to Status: solved upon solving — but the PR guard rejects any solution PR that edits a challenge statement file. Removing lifecycle fields (Status, Solution) from challenge_card() breaks that cycle, making the card stable regardless of the challenge's lifecycle state.

• python/lean_pool/challenge.py: Drops Status and Solution entries from the challenge_card() fields list; adds a docstring explaining the design rationale. The solution_card() function and the private _format_solution() helper are unchanged and still cover the solution-side card.
• Challenge/Mazur.lean and Challenge/Odlyzko.lean: Regenerated cards with Status: open removed, bringing the two existing open challenge files into sync with the new generator output.
• python/tests/test_challenge.py: Adds a regression test confirming that challenge_card() produces identical output for open and solved entries and contains no lifecycle fields.
• AGENTS.md, CLAUDE.md, CONTRIBUTING.md, .github/CODE_QUALITY.md: Documentation updated to explicitly state that statement files are not touched when solving a challenge.

Confidence Score: 5/5

Safe to merge — the change is self-contained, well-tested, and all two existing challenge cards have been regenerated to match the new format.

The root cause of the bug (lifecycle fields in a file that must stay immutable) is correctly addressed. The challenge_card() change is minimal and deterministic, the quality gate in quality.py already calls challenge_card() for its comparison so it automatically picks up the new format, and the two live challenge files have been regenerated. No existing tests were broken — the card test fixture never checked for Status: — and the new regression test directly encodes the contract that must hold going forward.

Files Needing Attention: No files require special attention. The core logic change is in python/lean_pool/challenge.py, which is straightforward. The two .lean card regenerations and documentation updates are consistent with each other.

Important Files Changed

Filename	Overview
python/lean_pool/challenge.py	Removes Status and Solution fields from challenge_card() output; adds explanatory docstring. _format_solution() remains in use by solution_card().
python/tests/test_challenge.py	Adds a focused regression test that verifies challenge_card() is idempotent across open/solved states and contains no lifecycle fields.
Challenge/Mazur.lean	Removes Status: open from the regenerated challenge card, matching the updated generator output.
Challenge/Odlyzko.lean	Removes Status: open from the regenerated challenge card, matching the updated generator output.
.github/CODE_QUALITY.md	Documents the new invariant: challenge cards carry no lifecycle fields, with a clear explanation of why.
AGENTS.md	Clarifies that solving a challenge leaves the challenge statement file byte-identical.
CLAUDE.md	Same single-sentence addition as AGENTS.md and CONTRIBUTING.md; kept in sync.
CONTRIBUTING.md	Same single-sentence addition as AGENTS.md and CLAUDE.md; kept in sync.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
    subgraph before["Before this PR (broken)"]
        A1[Contributor solves challenge] --> B1[Adds Solution/X.lean\nFlips registry to 'solved']
        B1 --> C1[Regenerates card\nchallenge_card adds 'Status: solved']
        C1 --> D1{PR guard check}
        D1 -->|Challenge statement edited| E1["❌ PR rejected\n(edits statement file)"]
        C1 --> F1[Skip regeneration,\nleave card stale]
        F1 --> G1{Card check}
        G1 -->|Card doesn't match registry| H1["❌ PR rejected\n(stale card)"]
    end
    subgraph after["After this PR (fixed)"]
        A2[Contributor solves challenge] --> B2[Adds Solution/X.lean\nFlips registry to 'solved']
        B2 --> C2[Regenerates card\nchallenge_card omits lifecycle fields]
        C2 --> D2[Card is byte-identical\nto the open version]
        D2 --> E2{PR guard check}
        E2 -->|Statement file untouched| F2["✅ PR passes"]
        D2 --> G2{Card check}
        G2 -->|Card matches registry| H2["✅ Card passes"]
    end

Loading

_{Reviews (1): Last reviewed commit: "Two gates I added contradicted each othe..." | Re-trigger Greptile}

[github-actions]

🤖 LLM review — challenge (gpt-5.6-sol)

Reviewed head: 83677c7366dfae280ad6577472a39e89dce04473

Verdict: ✅ approve

This is not a challenge-content change: it leaves Challenge.Mazur.torsion_ncard_le and Challenge.Odlyzko.abs_discr_ge, their informal statements, and their citations unchanged, and only removes lifecycle metadata from generated challenge cards. The existing entries concern significant named number-theory results, and this diff neither alters their mathematical contracts nor introduces a faithfulness, vacuity, or gameability issue.

Aspect	Value
Significance	✅ high
Faithful to the prose	✅ faithful
Matches cited source	🟡 unverifiable
Vacuity risk	✅ none
Difficulty	research
Estimated solution size	~0 lines — This PR introduces no theorem to prove and requires no Lean proof lines; the solution sizes of the unchanged existing challenges cannot be reassessed from this metadata-only diff.

Statement check: The diff changes no Lean proposition or informal statement; it only removes Status: open from the two affected cards.

Approve because the patch does not modify any challenge statement or its informal mathematical contract.

---

Tokens: 5,796 in / 1,827 out · Tier: flex · Effort: xhigh · Cost: $0.0419
Automated review against .github/CHALLENGE_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.