Conjecture run panel:

Build the corpus for a run

An engine is only as good as what it is allowed to read. This is the method that built the biophoton pack, reproduced end to end: a curated seed bibliography becomes a mapped publication universe, a clustered field structure, a mined statement corpus and a searchable knowledgebase. Bring the seed; the harness does the rest.

Intake

1. Intake: your seed bibliography

Method

2. The method, stage by stage

Each stage is idempotent and cached, so a rerun is free and a failure resumes rather than restarts. The hub's corpus builder (builder/run.py) runs A, B, C, E, the index, I, J and K; clustering (D) and the claim registry (M) are a pack's own tools, since engines never read the first and the second is curation.

Interface

3. What the corpus API exposes

Engines never touch the database. They see four calls, and nothing else.

search(query, limit, year_max)   full-text over title, abstract and body
get_work(work_id)                one record
statements(work_id, kind)        mined open-problem sentences
neighbors(work_id)               citing / cited within the universe

year_max exists so novelty can be scored honestly: restrict an engine to literature before a cutoff, then check its "new" hypotheses against what was actually published afterwards.

Sources & licences

Everything the harness reads or runs, and the terms it comes under. One engine carries a licence that restricts what may be published from its output; it is flagged.

Data

Corpus and data

Engines

Hypothesis engines

Licence, status and, behind Learn more on each row, what the architecture does, which seam this harness replaces to point it at our corpus, and the sources the description draws on.

Method

Verification

Configure a run

Pick the corpus, the engines that generate and the families that verify. The harness emits the commands. Engines needing an API key are shown but not selectable until one exists.

…

Hypotheses:

questions the field states about itself, every engine that has run on them, and every verdict against what they produced.

The ledger

Every hypothesis, and every verdict against it

One row per hypothesis. The judge columns are our own audit: does each reasoning step hold against the corpus it cites. The theoria column is independent of all of it: theoria never sees the citations or which engine wrote the hypothesis, only the arithmetic, which it re-derives from scratch. A hypothesis can pass our audit and still fail theoria's: where the two disagree is the reason for running both, and the ledger flags every such case as it lands.

Output

Generation

Signal

Cross-engine convergence

Where two independent model families reached the same claim in different vocabulary. Independent arrival is weak evidence that a hypothesis is findable in the literature rather than invented.

Signal

Conflicts: discriminating experiments

Pairs asserting incompatible things about the same measurand. One being right makes the other wrong, so each pair defines an experiment that would settle it.

Output

Certified hypotheses

Survived step-by-step audit under unanimity across all judge families, and judged not to be restatements of the existing registry.

Output

Declined

Published with reasons: the declines are the point of the exercise.

Verification

Every run ends here, and never with the model that generated. The discipline is adapted from theoria; the verifiers are then themselves measured, which is possible wherever a pack holds labelled ground truth, which no generator project has.

Discipline

1. The certification discipline

theoria is a verified-reasoning harness, not a benchmark suite. A claim must be emitted as a stepwise proof; independent judges audit every step; the answer is certified or declined, never quietly accepted. We adopt that discipline with one addition its author did not need: a citation step must resolve to a work that exists in this corpus and actually assert what the step claims.

Independent verifier

2. theoria, actually run

Sections 1 and 3 to 7 describe our own judges. This section is different: it is theoria itself, cloned and executed (its solver, interpreter, formalizer, per-step judges, pedantry filter and convention lift), not our imitation of its discipline.

It is given something deliberately narrow. We extract the steps an engine itself marked as computation, plus the estimand, and pose them as one self-contained proposition. theoria never sees the citations, the seed question, or which engine wrote it. It re-derives every number from scratch and rejects any step resting on an unstated premise, then answers CORRECT or INCORRECT with the specific error.

That makes it independent of our judges in the way that matters. Our judges ask a question about this corpus: does the cited paper support the step citing it. theoria asks whether the reasoning is valid at all. A hypothesis can be scrupulously cited and still arithmetically wrong, which is exactly the failure class the run turned up on the physics side.

What theoria can answer, and what each outcome means

theoria separates two questions that are usually conflated: did I produce a sound proof (its own audit of itself) and what does that proof conclude (the answer). Both are in every run record, and both are needed to read a verdict correctly.

How those become the ledger's theoria column

Fidelity to the upstream setup: stated, not assumed

Consumption, measured. Per claim: 31 to 92 LLM calls, mean 6.3M input tokens (4.2M of it prompt-cache reads) and 165k output, 22 to 35 minutes wall-clock. All 50 eligible claims project to roughly 315M input / 8M output tokens. Billed through the Codex CLI subscription: the run records' cost fields read zero throughout. Because a full sweep is about a day of continuous compute, runs are now launched per named claim: the adapter refuses --run without --only C001,… or an explicit --all, and the Run page's trigger submits only ticked claims.

Benchmark

3. Verifier benchmark, scored against known labels

Where a pack holds a verified claim register, the verifiers themselves can be scored: blinded items, each a scoped claim plus one verbatim sentence whose stance was already adversarially verified, with refutations over-represented so that a verifier that simply agrees with the field scores badly. Sentences quoted publicly are excluded, so nobody can answer from memory.

Headline

4. Do judges prefer their own model family?