From 83677c7366dfae280ad6577472a39e89dce04473 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Wed, 29 Jul 2026 00:06:11 -0700 Subject: [PATCH] Two gates I added contradicted each other, and solving a challenge was impossible to do cleanly: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - the PR guard **rejects a solution PR that edits a challenge statement** — the merged statement is the text comparator judges against; - the quality checker **rejects a stale challenge card**, and the card contained `Status:` and `Solution:`, both of which change the moment a challenge is solved. Regenerate the card and the guard refuses the PR. Leave it stale and the card check refuses it. [#301](https://github.com/Vilin97/lean-pool/pull/301) — the first real solution, the Odlyzko bound proved in a 210-file project — hit exactly this. The contributor did the right thing, with a commit titled *"fix: preserve the Odlyzko challenge statement"*, and the stale-card gate would have failed them for it. I found it by running our own gates against their branch: ``` Challenge/challenges.yml:1: challenge card for odlyzko-root-discriminant-bound is out of date ``` So the card now carries the *contract* and never the *lifecycle*: source, proposers, open declarations, tags, MSC, estimated size, and the informal statement each declaration is judged against. Status and the solution pointer live in `challenges.yml`, on the answering module's own card in `Solution/`, and in `make challenges`. The invariant is now a test: `challenge_card()` returns the same text for an open challenge and for the same challenge marked solved. The two existing cards are regenerated (one line each), and the docs say why. 🤖 Generated with [Claude Code](https://claude.com/claude-code) BODY Keep the challenge card free of lifecycle, so a challenge can be solved Two gates contradicted each other. The PR guard rejects a solution PR that edits a challenge statement, because the merged statement is the text comparator judges a solution against. The quality checker rejects a stale challenge card — and the card carried `Status:` and `Solution:`, both of which change when a challenge is solved. Regenerate the card and the guard refuses the PR; leave it stale and the card check refuses it. PR #301, the first real solution, hit exactly this: the contributor preserved the statement as the rules ask, and the stale-card gate failed them for it. The card now carries the contract and never the lifecycle — source, proposers, open declarations, tags, MSC, estimated size, and the informal statement each declaration is judged against. Status and the solution pointer live in the registry, on the answering module's card, and in `make challenges`. A test pins the invariant: the card is identical for an open challenge and the same challenge marked solved. Co-Authored-By: Claude Opus 5 --- .github/CODE_QUALITY.md | 1 + AGENTS.md | 2 +- CLAUDE.md | 2 +- CONTRIBUTING.md | 2 +- Challenge/Mazur.lean | 1 - Challenge/Odlyzko.lean | 1 - python/lean_pool/challenge.py | 13 ++++++++++--- python/tests/test_challenge.py | 17 +++++++++++++++++ 8 files changed, 31 insertions(+), 8 deletions(-) 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