Skip to content

collection_policy.md

Latest commit

 

History

History
108 lines (81 loc) · 4.6 KB

collection_policy.md

File metadata and controls

108 lines (81 loc) · 4.6 KB
Raw

Candidate collection and filtration policy

  • Policy version: 2
  • Status cutoff: 2026-07-24
  • Scope: runtime-neutral counterexample-search tasks

What belongs in the catalog

A catalog record freezes a mathematical claim and a falsification contract. It must not depend on Harbor, a particular agent interface, or a prompt template. Runtime packages are derived artifacts.

Every admitted candidate is evaluated against these gates:

  1. Exact claim: the record identifies one statement and one polarity.
  2. Finite refutation: falsity has a finite object or finitely encoded proof certificate.
  3. Terminating verification: the proposed checker always halts. Numerical evidence alone is insufficient.
  4. Status evidence: a dated primary, peer-reviewed, institutional, or expert-maintained source treats the formulation as open. Candidate records may carry pending while an independent literature audit is scheduled; only pass records can advance to reviewed.
  5. Duplicate review: equivalent formulations and implication clusters are identified before benchmark sampling.

Fame is useful for significance and provenance, but it never overrides a gate.

Verification tiers

  • A — direct witness: recompute every predicate on an explicit finite object.
  • B — exhaustive finite check: exact enumeration, dynamic programming, canonicalization, or exact optimization establishes a global finite claim.
  • C — proof-carrying: SAT/SMT/ILP certificates, formal proofs, rigorous intervals, normal surfaces, or another independently checkable proof object discharges the remaining obligation.

The tiers describe mechanics, not mathematical difficulty or probability.

Search profiles

The catalog records a coarse operational profile without estimating whether a conjecture is true:

  • direct-enumeration
  • constraint-search
  • exact-optimization
  • proof-carrying

This is the filtration proxy for counterexample exposure. The repository does not publish success percentages until the calibration protocol in CEPM-1 has passed its prospective release gate.

Source standard

Preferred evidence, in order:

  1. original papers and peer-reviewed research or surveys;
  2. primary preprints for the newest result;
  3. editor-maintained lists such as AIM problem lists, the Kourovka Notebook, Erdős Problems, The Open Problems Project, and EGRES Open;
  4. official institutional problem pages.

General encyclopedias and search snippets may aid discovery but do not by themselves advance a task to reviewed. Erdős Problems explicitly warns that its open status reflects the maintainer's current knowledge; records sourced there therefore retain an independent-review requirement.

Secondary aggregations such as UnsolvedMath may be pinned as broad discovery inputs, but their status labels, rewritten statements, difficulty ratings, and identifiers are not admission evidence. Promotion requires recovery of a primary or editor-maintained source. Identifier collisions and extraction damage remain explicit data-quality flags rather than being silently repaired.

Status changes

A credible proof or counterexample claim appends a quarantine event even before peer review. A new snapshot then makes the task ineligible; the historical task and snapshot are not rewritten. Restoring a task requires a later claim-dismissed or independent-status-review event with a source.

Status and execution are independent:

  • active, review-pending, and quarantined describe current eligibility;
  • design-only, prototype, and independently-tested describe verifier maturity.

The Erdős status audit compares represented problem numbers with its machine-readable maintainer feed. States described there as still open but finite (falsifiable, verifiable, and decidable) remain active status evidence. A transition to another state is a quarantine trigger, not an automatic declaration that a claimed result is correct. One source problem may support multiple canonical benchmark claims; the audit tracks all linked tasks and applies the same source-status transition to each of them.

Release gates

Candidate admission is intentionally weaker than benchmark release. Release also requires:

  • review of statement, polarity, and status by a relevant mathematician;
  • one primary verifier and an independently implemented reproduction checker;
  • malformed-output, near-miss, mutation, and planted-shadow tests;
  • frozen resource limits and a model/tool manifest;
  • leakage-family assignment and contamination review.

If fewer tasks pass, the release is smaller. Cardinality is not a reason to lower the gate.