Add sourced open-problem database layer

[anirudhabspk]

Base branch

This targets codex/200-unique-conjectures so the diff stays clean. It is meant to merge after #3 lands.

What this adds

A database/ layer that collects open problems from published upstream collections at volume, categorises them, and marks the subset a script can decide. Two layers in one record format: every row is reference material, and benchmark.eligible plus benchmark.verifier separate rows a verifier settles from rows a finite object merely could settle.

This is deliberately looser than tasks/catalog.json and never feeds it. Catalog admission still requires the gates in docs/collection_policy.md.

Contents

Source	Maintainers	Records	Scorable	Verifier
La Jolla Covering Repository	D. M. Gordon	250	250	poly
Bounds on linear codes (codetables.de)	M. Grassl, A. E. Brouwer	250	250	exhaustive-exp
Erdős problems	T. Bloom, T. Tao, contributors	43	0	none yet

543 records, 500 with a tested verifier. All rows are unsolved problems.

One verifier per class

A class is a family sharing one witness shape, so one verifier serves all of it. Adding rows adds no verifier work, which is what makes the benchmark layer scale. Validation rejects a class whose records disagree about their verifier.

The two classes stress different ends of the design: covering designs take a set of blocks and check in polynomial time; linear codes take a generator matrix and enumerate all 2^k codewords, which is why verifier_complexity exists.

Credit is a gate

Every source names its maintainers, records how they ask to be cited, and carries forward the caveats they state about their own data. Validation fails if any of it is missing, and docs/database.md is generated from it. The codetables cell pages credit Brouwer's earlier tables, so that upstream-of-upstream is credited too.

Evidence and auditing

Each row stores evidence.url and evidence.quote, verbatim text at that URL supporting the status claim, normalised by stripping tags and collapsing whitespace. scripts/audit_database.py re-fetches and looks for the quote; a row whose quote is absent from its own cited page does not match its source.

That gate caught a real defect during development. The Erdős rows quoted the crowdsourced YAML while citing erdosproblems.com, so nothing was verifiable at the address the row named. They now cite the authoritative problem page and quote the status banner printed on it, and the builder drops any row the site does not confirm. All 43 agreed on the last run.

Current audit: 543/543 quotes found.

Testing

Verifiers are tested against witnesses whose correct answer is already known, since no counterexample can be invented for an open problem:

• covering designs use the record coverings published by the source, which must be accepted as valid coverings and rejected as improvements on their own record, and must fail coverage when a block is dropped;
• linear codes use classical constructions whose minimum distance is a theorem, the [2^m-1, m, 2^(m-1)] simplex codes and the [n, 1, n] repetition codes.

Accept paths are exercised by relaxing the target, not by solving anything. VerifierContractTest discovers any future class verifier and requires it to reject junk rather than raise.

29 tests.

Offline re-derivation

Validation recomputes bounds rather than trusting the scrape: the Schonheim bound for every covering row, the Singleton bound for every code row. Codetables rows are additionally cross-checked against their own cell page at build time; 250/250 matched.

Scaling

Row counts are capped by constants at the top of each builder, not by the filters. Upstream has several thousand open cells per source. Fetches are cached under .cache/ and rate limited, so reruns are free and a crash resumes cheaply. Test fixtures are sampled rather than kept per row, so the committed diff stays reviewable as rows grow.

Known limits

• The 43 Erdős rows have no verifier. Each needs a bespoke predicate read off its own statement, and they are recorded as eligible-but-unimplemented rather than implying coverage that does not exist.
• Nothing here establishes that a problem is genuinely open. It records who says so, and where.
• Whether a model can beat any of these records is unmeasured. A baseline run on a sample is the next step.

Validation

python3 scripts/validate_database.py --check
python3 -m unittest discover -s tests
python3 scripts/audit_database.py --sample 25 --no-cache   # needs network

CI runs the first two. The builder and the auditor need network and are run by hand.