Skip to content

feat: validate the problem bank index against its catalogs - #622

Closed
bazz1111 wants to merge 1 commit into
TheJustinSunPrize:mainfrom
bazz1111:problem-bank-validation
Closed

bazz1111 wants to merge 1 commit into
TheJustinSunPrize:mainfrom
bazz1111:problem-bank-validation

Conversation

@bazz1111

@bazz1111 bazz1111 commented Sep 17, 2026 •

Copy link
Copy Markdown

Note on the template. The repository's PR template was replaced with a solver/Lean submission form in #646, after this PR was opened. This change is tooling — it adds a validator and corrects one index row — so the sections below follow the template that was in place when it was opened.

Change

The problem bank is the largest hand-maintained asset in this repository — 1,022 index rows across eleven volumes — and nothing checked it.

links verifies that an anchor exists, not that it belongs to the row citing it. The most common hand-editing mistake, a copied row whose anchor still points at the previous problem, passed both links and validate:

$ python scripts/manage.py links      -> links: OK
$ python scripts/manage.py validate   -> validate: OK
# after editing JSP-000038 to link #JSP-000039

problems/README.md also states several precise, machine-checkable facts about itself, none of which were enforced: the total count, consecutive numbering, volume boundaries, the eligibility rule, the claim-status lifecycle, and the number of records carrying an Attribution basis row. Meanwhile the catalog is edited constantly — the last eleven commits are all docs: changes to it — while scripts/manage.py has not been touched since the initial commit.

This adds a problems command that asserts exactly those statements and nothing more. The counts are read from the index prose rather than duplicated in the script, so a curator who edits the claim is held to it:

  • the No. column runs consecutively from JSP-000001 to the documented total;
  • every row links its own anchor, in the volume that covers its number;
  • the index title matches the catalog heading, and every record has a detail table, an explicit anchor and a place in the index;
  • Eligible to claim is Yes exactly when Current status is Solved and Lean proof is Yes; Pending verification stays a screening judgement;
  • Claim status is Unavailable unless the record is eligible, so the documented Unavailable → Unclaimed → Claimed lifecycle holds;
  • the index and the detail table agree on eligibility, status and Lean proof;
  • the counts stated in the prose match the catalog.

The Lean proof rule follows the documented field shape: a status is stated alone or extended with — and its sources, because the field "combines the proof status, source links, and formalization contributor credits". A qualification value is instead reproduced with the wording the index states it preserves, which is why Reported; standalone source not located and its fuller detail wording are listed as a pair rather than loosening the rule for every record.

Enforcement needs no workflow change: tests/test_problems.py ends with the same check applied to the bank this repository actually publishes, and python -m unittest discover -s tests is already a step in the Validate workflow, so index drift now fails CI on every push and PR. If you would rather see it as its own named step, adding one line to .github/workflows/validate.yml is straightforward.

Compatibility with the correction already in flight. Issue #569 / PR #574 propose reclassifying JSP-000448: Eligible to claim from Pending verification to Yes, Claim status from Unavailable to Unclaimed, and the documented attribution count from 66 to 67. Running this check against the state PR #574 produces, with the JSP-000037 correction from this PR applied, reports problems: OK — the check accepts that correction instead of blocking it. Two of the rules have the shape they do because of that record: Pending verification is treated as a third legal value, and the index's short qualification wording is accepted alongside the catalog's fuller phrasing.

Running the new check against the current bank found one record that contradicts itself. JSP-000037 still carried the former "Yes" screening flag in its Lean proof field — . Yes — — although the same record states in Eligibility scope:

The former n≥3 entry carried a Yes screening flag. That flag does not transfer to the combined unresolved entry or to dimension two.

Its index status was also Progress (not fully resolved), the only non-standard status word among 1,022 rows (Progress 417, Solved 354, Open 250). Commit 727aff7, which capitalised the claim-status values, rewrote all 1,026 index lines and missed this one; the phrase itself came from a6ee64e. Both are corrected here.

Evidence that the check is load-bearing — with the JSP-000037 correction reverted:

$ python scripts/manage.py problems          # before the correction
ERROR: problems/README.md: JSP-000037 Current status must be one of Open, Solved, Progress
$ python scripts/manage.py problems          # after the correction
problems: OK

Record or policy impact

JSP-000037 is edited in two places: the index status Progress (not fully resolved) becomes Progress, and the detail Lean proof value loses the stale . Yes — marker. Its Eligible to claim stays No and its Claim status stays Unavailable, so no screening outcome, nomination or award eligibility changes. The record's own Eligibility scope row already states that the former flag does not transfer, so this aligns the field with the text beside it.

No other record changes. The new check confirms that the remaining 1,021 rows already satisfy every rule, so this is a guard rail for future edits rather than a correction of current data. No schema, status transition or published decision changes.

Checks

  • All text is in English; candidate text does not announce an award.
  • Unconfirmed recipient identities use placeholders in every file and commit; no private contacts, payment details, assessment criteria or deliberations appear in files or commit history.
  • Verification artifacts are externally archived with ID, SHA-256, and byte count. (Not affected: this PR touches no verification artifact.)
  • Published statements and decisions are preserved; replacements and revocations retain history.
  • python scripts/manage.py validate and python scripts/manage.py links pass.
  • python scripts/manage.py build has run and python scripts/manage.py check passes.
  • Relevant validator tests pass; any validation limits are explained.
$ python scripts/manage.py validate
validate: OK
$ python scripts/manage.py links
links: OK
$ python scripts/manage.py problems
problems: OK
$ python scripts/manage.py build
build: OK
$ python scripts/manage.py check
check: OK
$ python scripts/manage.py history --base f4e7173d89dfe91022a185427d63452c8ffbf6ae
history: OK
$ python -m unittest discover -s tests
Ran 46 tests
FAILED (failures=2, errors=1)

Validation limits: all 24 new problem-bank tests pass. The three failures are pre-existing and unrelated to this change — two are the Windows path-separator defect fixed separately in #608 (test_published_statement_immutable_and_superseded, test_revocation_keeps_original_evidence), and one (test_symlinks_and_misplaced_records_rejected) needs symlink privileges this host does not grant. CI runs on ubuntu-latest, where the suite is green. build leaves no diff under data/.

Reviewer decision

The problem bank is the largest hand-maintained asset in this repository —
1,022 index rows across eleven volumes — and nothing checked it. `links`
verifies that an anchor exists, not that it belongs to the row that cites it,
so the most common hand-editing mistake (a copied row whose anchor still
points at the previous problem) passed both `links` and `validate`:

    | JSP-000038 | [Sendov conjecture](catalog-0001-0100.md#JSP-000039) | ...   # accepted

`problems/README.md` also states several precise, machine-checkable facts about
itself, none of which were enforced: the total count, consecutive numbering,
volume boundaries, the eligibility rule, the claim-status lifecycle, and the
count of records carrying an `Attribution basis` row.

Add a `problems` command that asserts exactly those statements and nothing
more. The counts are read from the index prose rather than duplicated in the
script, so a curator who edits the claim is held to it:

- the `No.` column runs consecutively from JSP-000001 to the documented total;
- every row links its own anchor, in the volume that covers its number;
- the index title matches the catalog heading, and every record has a detail
  table, an explicit anchor and a place in the index;
- `Eligible to claim` is `Yes` exactly when `Current status` is `Solved` and
  `Lean proof` is `Yes`; `Pending verification` stays a screening judgement;
- `Claim status` is `Unavailable` unless the record is eligible, so the
  documented `Unavailable -> Unclaimed -> Claimed` lifecycle holds;
- the index and the detail table agree on eligibility, status and Lean proof;
- the counts stated in the prose match the catalog.

The Lean proof rule follows the documented field shape: a status is stated
alone or extended with " — " and its sources. A qualification value is instead
reproduced with the wording the index states it preserves, which is why
`Reported; standalone source not located` and its fuller detail wording are
listed as a pair rather than loosening the rule for every record.

Running the new check against the current bank found one record that
contradicts itself. `JSP-000037` still carried the former "Yes" screening flag
in its `Lean proof` field — `. Yes —` — although the same record states in
`Eligibility scope` that "the former n≥3 entry carried a Yes screening flag.
That flag does not transfer to the combined unresolved entry or to dimension
two". Its index status was also `Progress (not fully resolved)`, the only
non-standard status word among 1,022 rows (417 `Progress`, 354 `Solved`,
250 `Open`); commit 727aff7, which capitalised the claim-status values, rewrote
all 1,026 index lines and missed this one. Both are corrected here. The
record's `Eligible to claim` stays `No`, so no screening outcome changes.

Validation (Windows, Python 3.13), with the JSP-000037 fix reverted to show the
check is load-bearing:

    $ python scripts/manage.py problems          # before the fix
    ERROR: problems/README.md: JSP-000037 Current status must be one of Open, Solved, Progress
    $ python scripts/manage.py problems          # after the fix
    problems: OK

    $ python scripts/manage.py validate   -> OK
    $ python scripts/manage.py links      -> OK
    $ python scripts/manage.py build      -> OK, no diff under data/
    $ python scripts/manage.py check      -> OK
    $ python scripts/manage.py history --base f4e7173 -> OK
    $ python -m unittest discover -s tests: 46 tests, 2 failures and 1 error
      All 24 new problem-bank tests pass. The three failures are pre-existing
      and unrelated to this change: two are the Windows path-separator defect
      fixed in TheJustinSunPrize#608, and one needs symlink privileges the host does not grant
      (CI runs on ubuntu-latest, where the suite is green).

`tests/test_problems.py` builds a small synthetic bank and asserts each rule
independently, including the two accepted shapes (credited detail status, and
the documented qualification wording) so the rules cannot silently tighten. A
final test applies the same check to the bank this repository actually
publishes, so the existing `python -m unittest discover -s tests` CI step fails
whenever the index and its catalogs drift apart. Enforcement therefore needs no
workflow change.
@bazz1111

Copy link
Copy Markdown
Author

Closing this PR myself. It no longer applies after #762 ("docs: simplify problem catalog status and presentation") reworked the same catalog/index surface this branch touches, so the merge conflict cannot be resolved into anything coherent without re-doing the work on a different basis.

Per the current CONTRIBUTING.md guidance ("Use issues for other corrections or requests rather than changing unrelated repository files"), the still-open concern from this branch is tracked as issue #815 instead.

No maintainer action needed here.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant