diff --git a/.github/CODE_QUALITY.md b/.github/CODE_QUALITY.md index 01ef337996..80cd2c37a4 100644 --- a/.github/CODE_QUALITY.md +++ b/.github/CODE_QUALITY.md @@ -57,6 +57,7 @@ Challenge-mode checks (the `Challenge/` library — open statements awaiting a p - `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 diff --git a/AGENTS.md b/AGENTS.md index d15e17b425..3135aa5b2e 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -98,7 +98,7 @@ A challenge PR gets its own [LLM review](.github/CHALLENGE_REVIEW_RULES.md), whi 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/.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/.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: diff --git a/CLAUDE.md b/CLAUDE.md index d15e17b425..3135aa5b2e 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -98,7 +98,7 @@ A challenge PR gets its own [LLM review](.github/CHALLENGE_REVIEW_RULES.md), whi 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/.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/.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: diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index d78ebddd3d..33cf9f1382 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -33,7 +33,7 @@ A challenge PR gets its own [LLM review](.github/CHALLENGE_REVIEW_RULES.md), whi 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/.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/.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: diff --git a/Challenge/Mazur.lean b/Challenge/Mazur.lean index 34cfe9ea34..1259b2f0f4 100644 --- a/Challenge/Mazur.lean +++ b/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 diff --git a/Challenge/Odlyzko.lean b/Challenge/Odlyzko.lean index a8f6991e7d..983ece8fb8 100644 --- a/Challenge/Odlyzko.lean +++ b/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 diff --git a/python/lean_pool/challenge.py b/python/lean_pool/challenge.py index 4b0f5ef06e..e467fb8d27 100644 --- a/python/lean_pool/challenge.py +++ b/python/lean_pool/challenge.py @@ -311,12 +311,21 @@ def challenge_card(challenge: dict[str, Any]) -> str: 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 @@ def challenge_card(challenge: dict[str, Any]) -> str: 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:"]) diff --git a/python/tests/test_challenge.py b/python/tests/test_challenge.py index 29956d8382..95ed389ed8 100644 --- a/python/tests/test_challenge.py +++ b/python/tests/test_challenge.py @@ -585,3 +585,20 @@ def test_option_audit_still_reports_combined_findings(tmp_path: Path) -> None: 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