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

.github/CODE_QUALITY.md

@@ -1,3 +1,3 @@
 # Code Quality Automation
 
 Lean Pool uses deterministic CI for mechanical quality checks and LLM review for judgment calls. This page separates checks that are enforced today from planned automation.
@@ -57,6 +57,7 @@
 - `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
+- a challenge card carries no lifecycle: no `status`, no solution pointer. A statement file must not change once merged, and the PR guard rejects a solution PR that edits one — so a card that moved with the status would make solving a challenge impossible (regenerate it and the guard refuses the PR; leave it stale and the card check refuses it). The solved state lives in the registry, on the answering module's card, and in `make challenges`
 - `#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
 

AGENTS.md

@@ -1,3 +1,3 @@
 This file is a concatenation of README.md and CONTRIBUTING.md.
 
 <p align="center">
@@ -98,7 +98,7 @@
 
 A challenge statement never changes once merged: it is the text every solution is judged against. So a solution goes in [`Solution/`](Solution/) as its own module, which **restates** the statement under the same name and proves it. It must not import the challenge module — comparator exports the two environments separately and checks that the statements agree, and importing would defeat exactly that check (a gate enforces it).
 
-Open a content PR that adds `Solution/<Challenge>.lean` and flips the registry entry to `status: solved` with a `solution:` block (`module:`, plus optional `authors:`, `project:`, and `verified:`), then regenerate the index and cards. A solution that needs real work should prove it in a pooled project under `LeanPool/` and leave a thin bridge here.
+Open a content PR that adds `Solution/<Challenge>.lean` and flips the registry entry to `status: solved` with a `solution:` block (`module:`, plus optional `authors:`, `project:`, and `verified:`), then regenerate the index and cards. The challenge statement file is **not** touched by any of that: its card carries the contract (source, proposers, open declarations, the informal statement) and never the lifecycle, so solving a challenge leaves it byte-identical. A solution that needs real work should prove it in a pooled project under `LeanPool/` and leave a thin bridge here.
 
 Correctness is decided by [`leanprover/comparator`](https://github.com/leanprover/comparator), which replays the solution through the Lean kernel and checks that it proves *the same* statement with no axiom beyond `propext`/`Quot.sound`/`Classical.choice`. [`challenge-verify.yml`](.github/workflows/challenge-verify.yml) runs it on every solved challenge in CI, with `landrun`, `lean4export`, and comparator pinned to exact commits. Locally:
 

CLAUDE.md

@@ -1,3 +1,3 @@
 This file is a concatenation of README.md and CONTRIBUTING.md.
 
 <p align="center">
@@ -98,7 +98,7 @@
 
 A challenge statement never changes once merged: it is the text every solution is judged against. So a solution goes in [`Solution/`](Solution/) as its own module, which **restates** the statement under the same name and proves it. It must not import the challenge module — comparator exports the two environments separately and checks that the statements agree, and importing would defeat exactly that check (a gate enforces it).
 
-Open a content PR that adds `Solution/<Challenge>.lean` and flips the registry entry to `status: solved` with a `solution:` block (`module:`, plus optional `authors:`, `project:`, and `verified:`), then regenerate the index and cards. A solution that needs real work should prove it in a pooled project under `LeanPool/` and leave a thin bridge here.
+Open a content PR that adds `Solution/<Challenge>.lean` and flips the registry entry to `status: solved` with a `solution:` block (`module:`, plus optional `authors:`, `project:`, and `verified:`), then regenerate the index and cards. The challenge statement file is **not** touched by any of that: its card carries the contract (source, proposers, open declarations, the informal statement) and never the lifecycle, so solving a challenge leaves it byte-identical. A solution that needs real work should prove it in a pooled project under `LeanPool/` and leave a thin bridge here.
 
 Correctness is decided by [`leanprover/comparator`](https://github.com/leanprover/comparator), which replays the solution through the Lean kernel and checks that it proves *the same* statement with no axiom beyond `propext`/`Quot.sound`/`Classical.choice`. [`challenge-verify.yml`](.github/workflows/challenge-verify.yml) runs it on every solved challenge in CI, with `landrun`, `lean4export`, and comparator pinned to exact commits. Locally:
 

CONTRIBUTING.md

@@ -1,3 +1,3 @@
 # Contributing to Lean Pool
 
 Lean Pool welcomes serious, medium- to large-scale formalizations of mathematics and related disciplines (see [`MOTIVATION.md`](MOTIVATION.md)). Browse [`LeanPool/`](LeanPool/) for examples and [`candidates/CRITERIA.txt`](candidates/CRITERIA.txt) for what we include.
@@ -33,7 +33,7 @@
 
 A challenge statement never changes once merged: it is the text every solution is judged against. So a solution goes in [`Solution/`](Solution/) as its own module, which **restates** the statement under the same name and proves it. It must not import the challenge module — comparator exports the two environments separately and checks that the statements agree, and importing would defeat exactly that check (a gate enforces it).
 
-Open a content PR that adds `Solution/<Challenge>.lean` and flips the registry entry to `status: solved` with a `solution:` block (`module:`, plus optional `authors:`, `project:`, and `verified:`), then regenerate the index and cards. A solution that needs real work should prove it in a pooled project under `LeanPool/` and leave a thin bridge here.
+Open a content PR that adds `Solution/<Challenge>.lean` and flips the registry entry to `status: solved` with a `solution:` block (`module:`, plus optional `authors:`, `project:`, and `verified:`), then regenerate the index and cards. The challenge statement file is **not** touched by any of that: its card carries the contract (source, proposers, open declarations, the informal statement) and never the lifecycle, so solving a challenge leaves it byte-identical. A solution that needs real work should prove it in a pooled project under `LeanPool/` and leave a thin bridge here.
 
 Correctness is decided by [`leanprover/comparator`](https://github.com/leanprover/comparator), which replays the solution through the Lean kernel and checks that it proves *the same* statement with no axiom beyond `propext`/`Quot.sound`/`Classical.choice`. [`challenge-verify.yml`](.github/workflows/challenge-verify.yml) runs it on every solved challenge in CI, with `landrun`, `lean4export`, and comparator pinned to exact commits. Locally:
 

Challenge/Mazur.lean

@@ -12,7 +12,6 @@ import Mathlib.GroupTheory.Torsion
 
 Source: doi:10.1007/BF02684339, url:https://www.numdam.org/item/?id=PMIHES_1977__47__33_0
 Proposed by: Kevin Buzzard, Vasily Ilin
-Status: open
 Open declarations: `Challenge.Mazur.torsion_ncard_le`
 Tags: elliptic-curves, torsion, modular-curves, flt-assumption
 MSC: 11G05, 11G18

Challenge/Odlyzko.lean

@@ -12,7 +12,6 @@ import Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
 
 Source: url:https://www.numdam.org/item/SDPP_1976-1977__18_1_A6_0/
 Proposed by: Kevin Buzzard, Vasily Ilin
-Status: open
 Open declarations: `Challenge.Odlyzko.abs_discr_ge`
 Tags: number-theory, discriminants, number-fields, flt-assumption
 MSC: 11R29, 11R42

python/lean_pool/challenge.py

@@ -1,3 +1,3 @@
 """Challenge mode: the registry, cards, and comparator configuration.
 
 Lean Pool's ``Challenge/`` library holds *open* statements — theorems (and
@@ -311,12 +311,21 @@
     the LLM reviewer) can judge faithfulness without leaving the file.
     ``lean_pool.quality`` regenerates and gates it, so the format has to be
     deterministic.
+
+    It deliberately carries none of the challenge's *lifecycle* — no
+    status, no solution pointer. Those live in the registry, because a
+    statement file must not change once merged: it is the text every
+    solution is judged against, and the PR guard rejects a solution PR
+    that edits it. Putting `status: solved` in the card would have made
+    solving a challenge impossible — regenerate the card and the guard
+    refuses the PR, leave it stale and the card check refuses it. The
+    solved state is recorded in `challenges.yml`, on the answering module's
+    own card, and by `make challenges`.
     """
     lines = [f"# {challenge['title']}", ""]
     fields = [
         ("Source", _format_source(challenge["source"])),
         ("Proposed by", _join(challenge["proposers"])),
-        ("Status", str(challenge["status"])),
         ("Open declarations", _join_declarations(challenge)),
         ("Tags", _join(challenge["tags"])),
         ("MSC", _join(challenge["msc"])),
@@ -325,8 +334,6 @@
         estimated = challenge["estimated_lines"]
         unit = "line" if estimated == 1 else "lines"
         fields.append(("Estimated size", f"~{estimated} {unit} of Lean"))
-    if challenge.get("solution") is not None:
-        fields.append(("Solution", _format_solution(challenge["solution"])))
     for label, value in fields:
         lines.extend(_wrap(f"{label}: {value}"))
     lines.extend(["", "Informal statement:"])

python/tests/test_challenge.py

@@ -1,3 +1,3 @@
 """Tests for challenge mode: registry, cards, comparator configuration, and gates."""
 
 from __future__ import annotations
@@ -585,3 +585,20 @@
 
     assert len(errors) == 1
     assert "declares an axiom" in errors[0].message
+
+
+def test_challenge_card_does_not_change_when_the_challenge_is_solved() -> None:
+    """Solving a challenge must not require editing its statement file.
+
+    The PR guard rejects a solution PR that edits a challenge statement,
+    and the card check rejects a stale card — so any lifecycle field in
+    the card makes solving a challenge impossible to do cleanly. PR #301
+    hit exactly that: the contributor preserved the statement, as the
+    rules ask, and the stale-card gate failed them for it.
+    """
+    open_card = challenge.challenge_card(CHALLENGE_ENTRY)
+    solved_card = challenge.challenge_card(_solved_entry())
+
+    assert open_card == solved_card
+    assert "Status:" not in open_card
+    assert "Solution:" not in open_card