The Case

Software engineers saw the shift first. They could place generated code in a repository, run tests, review the diff, and retain the result with its history. Mathematicians now face a related test. Models can propose proofs, formalizations, and finite constructions; kernels and frozen verifiers can check some outputs exactly. Researchers must still match each formal statement to the intended problem, establish novelty, integrate the result, and choose the next worthwhile question.

Empirical researchers face scarce experiments, noisy measurements, and separate authority over action. Models already draft protocols and search large literatures. Autonomous laboratories can close narrow model-to-bench loops. These systems can generate more candidates than reviewers and laboratories can assess.

As models make candidates cheaper, researchers spend more effort on selection and maintenance. Someone must decide what survives scrutiny, retain useful failures, and connect corrections to the claims they change. The next researcher or model inherits those decisions.

Researchers still document much of that work in prose. Papers hold claims and reasoning, but individual findings rarely keep a stable identity through later corrections. Registries, living reviews, provenance standards, and retrieval systems cover parts of the path. Failed runs remain in private threads. An agent’s synthesis can disappear with its context window, forcing the next worker to reconstruct the same state.

A writable frontier record would hold scoped findings, failed attempts, proposed and accepted changes, declared dependencies, and open obligations under a named policy and authority. Software has unusually strong versions of this machinery because code is digital, replay is cheap, and many tests are exact. Scientific fields need different tests, but they can still give each correction an address and a reviewable history.

Registry policy determines which histories later users can inspect. The record shows what a particular authority accepted, under which standard, and against which root; it does not settle truth or consensus. A public implementation therefore needs a forkable protocol and stewardship independent of any dominant client. Publishing source code while keeping the useful registry closed would leave the effective institution private.

The record would also become part of the corpus used by people and models. Mathematics offers the near-term case: exact checks can make constructions, formal proofs, failed routes, and open obligations cumulative while leaving significance and acceptance to judgment. Biology offers a related precedent. The PDB helped later systems learn alongside sequence databases, algorithms, compute, benchmarks, expertise, and institutional rules. In both cases, durable objects make accumulated work easier to inspect and correct.

We can test the idea first on a bounded problem in extremal combinatorics. OEIS records improved bounds on that problem, while local formal frontiers and frozen verifiers make specific results reproducible. This combination demonstrates receipts, exact checking, and replayable state in one domain. A general loop with independent producers remains unproven.

An empirical test would use a bounded frontier in materials or biology, a chartered registry, a few laboratories, a review window, and funding tied to deposits of failed protocols and corrections. A physical run produces evidence for reviewers. They judge the proposed state change; separate authorities control experiments, manufacturing, regulation, and clinical protocols. Success means that an accepted correction changes a later decision that would otherwise have used an obsolete assumption.

Vela currently provides the protocol and state layer. Its general runtime, empirical writeback, federation, and institutional propagation remain partial or proposed. A science gigafactory would add repeatable physical execution under separate authorization and return the resulting evidence for review.

The trilogy assigns each layer a separate job. Constellations of Borrowed Light makes the moral and epistemic argument for a shared record. The Discovery Engine describes the operating loop that turns activity into governed state. Gigafactories for Science follows that state into authorized physical work. The whitepaper specifies the protocol.