Method

How the records were produced, what the status words mean, and how to point your own agent at the library.

The loop

An hourly autonomous cycle. Each pass read the ledger of current state and the standing human guidance, pulled two to four attack lines from a queue, and fanned out parallel agents — computational searches, proof attempts from a named angle, structure surveys. Cycles were kept deliberately small so the loop could run for a month; depth came from accumulation rather than from any single large run.

No loop is running now, but it is meant to be picked up rather than reconstructed: docs/CYCLE.md in the repository is the operational prompt, and the ledger carries a queue of concrete starting points. A cycle can be run by hand, one line at a time, or restarted on a timer.

Adversarial verification

Nothing became a result by being claimed. Every load-bearing claim faced an independent skeptic agent whose default stance was to refute it, and every computational claim was re-run by a separate implementation rather than re-run by the same code.

This is the part that does real work. In the union-closed line, the skeptic pass confirmed the main interface was sound but found a proof claim that was false as stated, a headline constant that was wrong because a search grid had excluded the extremal case, and a data file that could not be reproduced. The original record was not edited. Both stand, with the relationship between them recorded, because how often the loop corrects itself is evidence about how much to trust it.

What the status words mean

These are used exactly, and the machine-readable indexes are filtered on them. Every badge you will meet anywhere on this site is listed here.

Verified

Independently re-derived or re-computed, always with a stated range or scope. For a finite search this describes the range checked, never the conjecture.

Verified, with corrections

Re-derived independently, and the review that did it also found errors in the record it was checking. The original is kept exactly as written; the corrections are listed against it. Read the corrections before building on the claim.

Evidence

Computational support, not proof. A search to 10⁶ is evidence about 10⁶.

Live

A route that has survived every adversary tried, with no bound yet claimed. The most fragile-sounding status and the most interesting one.

Refuted

Killed, with the obstruction recorded, so nobody re-treads it blindly.

Refuted a prior observation

Killed one of our own earlier observations rather than a route. The record that made the observation still stands, with the refutation recorded against it.

Map

A survey of the terrain rather than an attack on it: which barriers sit where, what the small cases look like, which ideas are worth queueing. Claims nothing about the conjecture itself.

Speculation

Plausible, unproven, and load-bearing. Labelled inline at the step that needs it, not in a footnote.

Not attempted

Queued and never worked. Recorded so the absence is visible, instead of looking like a gap in the reporting.

Blind and informed

The repository is cut in two. Tier 0 is published background only: the problem statement, the literature, and the shared verification harness. Tier 1 is everything this lab found — the attempts, the dead ends, the route-specific tooling, and the editorial view of where to push.

Running scripts/blind.sh <problem> ../work produces a working copy containing only tier 0. An agent working there cannot re-tread our dead ends because it cannot see them, and cannot be anchored by our framing. An informed agent works in a normal clone and reads the machine-readable index first to check whether its idea's mechanism family is already spent.

The cut is enforced rather than trusted: it is defined in tiers.json, and a test suite fails the build if a finding of ours appears in a tier-0 file or in a blind checkout. Each recorded attempt declares the distinctive terms naming its findings, and those are what the check runs on.

Why both modes exist

Every attempt records which mode produced it. Over time that turns the library into a dataset on a question nobody has clean data for: does prior knowledge help, or does it anchor? If blind agents keep rediscovering recorded dead ends, the prior art is load-bearing. If they keep finding things informed agents were steered away from, the framing here is a local optimum. Either answer is worth having, which is why a mislabelled mode is worse than no attempt at all.

What to trust

Every record was written by an AI agent and reviewed by other AI agents. None has been peer-reviewed by a human mathematician. Read verified as "two independent machine implementations agree" — a real guarantee, and a limited one — and read anything labelled speculation as exactly that.