A persistent research environment.

The research layer around frontier models

Catenation uses frontier models inside a persistent scientific working environment. The model supplies research judgment; the runtime supplies execution, context programs, tool calls, and recursive sessions; the domain harness supplies target identity, evidence relationships, and acceptance rules.

A scientific insight may first appear as a failed construction, a useful reduction, a counterexample, a calculation, or a new connection to a source. The system preserves those intermediate objects with the project, so another person or AI agent can inspect, challenge, and extend them. A finished proof or manuscript is one output of a longer, inspectable research process.

Model connections and authentication

Model configuration is separate from durable research state. Teams can switch configured providers while retaining their targets, evidence, and model provenance. Deployment profiles connect the chosen model, authentication, and tool interface.

The original September 21 fleet recordings use Astra through an authenticated remote connection. The expanded biology recording uses a locally hosted open-weight 27B model on NCShare, with four concurrent model calls shared by the agent queue. The native sessions run in separate CPU allocations.

Our evaluation focuses on useful research results, faithful reconstruction of prior work, correct handling of evidence changes, and the effort required to inspect outputs. The evaluation record brings together benchmark results, captured workloads, reproducible methods, and system checks.

Programmable context in a persistent REPL

The model-facing execution surface is IPython: a persistent Python REPL. Variables, imports, functions, intermediate results, and admitted agent handles remain available across turns. The model can write a context program that searches a corpus, inspects exact records, computes over selected material, and returns a focused result to its language context.

from fractions import Fraction
from mantis_forge import ctx

# retrieve a bounded source selection and its resource map
sources = await ctx.search("boundary cases", limit=4)
source_map = await ctx.cartography()

# ordinary working objects remain in this kernel
weights = [Fraction(1, 3), Fraction(2, 3)]
mass = sum(weights)

# a later turn can reuse the objects
assert mass == 1
print({"total": str(mass), "sources": len(sources)})

The runtime's context bridge also provides inspection of exact resource revisions, structural diffs, bounded dataset slices, filtering, provenance-linked derivation, collections, and pinning. These are function calls over external research state. The model decides what to materialize, transform, and show in the next prompt.

Compaction and kernel state have separate lifecycles. Conversation summaries preserve access to the live namespace and retained worker registry. Durable resource records, saved artifacts, and campaign snapshots support reconstruction when a kernel restarts.

Recursive teams through function calls

Delegation uses the same programmable environment as ordinary research. agents.spawn admits a child and returns a handle containing its identity, name, session directory, and model. The child has its own context, kernel, and transcript; the parent can continue useful work before collecting a result.

from mantis_forge import agents
import agent_message

worker = await agents.spawn(
    "Search for a counterexample under the locked assumptions.",
    name="boundary-check",
)

# follow up through the host-owned message router
await agent_message.send(
    "Check the zero case before the general construction.",
    receiver_role="child",
    receiver_name=worker.name,
)

# the parent can perform other work before waiting
children = await agents.list()
completed = await agents.wait(worker)

The message bridge addresses a parent, a named child, or a named sibling; a separate broadcast form targets the permitted agent family. The host owns routing, sender identity, and delivery receipts. Retained workers can be revisited through later messages, and agents.delete removes a child from the retained registry. Admission, message delivery, and scientific completion are distinct events.

A route records a durable research approach. A root session binds execution to its goal version, target hash, role, and assigned subject. The adaptive director uses the open frontier, existing ownership, activity observations, and certification debt to propose discovery, falsification, certification, incorporation, or recovery work. The model chooses research tactics inside that allocation.

Returned objects can include a precise lemma, a refuting witness, a source-backed observation, an executable calculation, or a statement of the unresolved step. Recursive execution makes those investigations concurrent; recording and reviewing their scientific meaning remains a separate operation.

Continual harness refinement

The runtime carries an editable layer of reusable behavior around each AI agent. It maintains four entry kinds: supplemental prompt notes, durable memories, executable skills, and subagent role specifications. A trajectory review can propose a small, evidence-backed change to that layer.

The state can be read and inspected; edit proposals support create, update, and delete. Every entry carries identity, scope, timestamps, version, and provenance. Local entries are combined with global state for the current session, while automatic trajectory refinement is directed toward local changes. Global promotion is explicit.

from mantis_forge import harness

await harness.refine(
    "Use the observed boundary failure to improve the local "
    "reviewer role. Retain the exact scope of the observation."
)
status = await harness.status()

Planning is separated from application. At commit time, the runtime compares the current entry with the baseline captured before planning and rejects conflicting edits. Structural validation checks the edit action and kind, required fields, and the callable description for skills. The base system prompt is protected.

Refinement results retain the applied edits, before-and-after entries, checksums, scope, and rollback identity. Session-local history and explicit global history support inspection and reversal. Refinement operates on the agent’s prompts, memory, skills, and roles. The evidence ledger continues to decide which claims and reviews belong to the research record.

Catenation’s RLM management combines a persistent programmable context with recursive agent execution and inspectable harness state.

Source-separated research scouting

The accompanying mathematics, physics, and computational-biology scouting workflows begin with literature evidence. Corpus builders retrieve Crossref and OpenAlex metadata, retain the raw provider responses, and reconcile records while preserving coverage and provenance. Source data and research synthesis remain distinguishable throughout the funnel.

A rejected direction remains useful: its source collision, obstruction, or failed test explains why later work should start elsewhere. A surviving dossier provides a concrete handoff rather than a free-form suggestion to “research this topic.” Each campaign begins with a current source audit and a precise target lock.

The dynamic dependency graph

The SQLite ledger records targets, routes, claims, obligations, artifacts, computations, reviews, checkpoints, and events. Its dependency graph keeps the relationships between research objects explicit. A promising calculation or failed construction can be retained as an intermediate artifact before there is a complete argument.

Target amendments create a new version and hash. Claims carry both an evidence grade and current validity, so a historically exact result can later be retracted or invalidated while retaining its original provenance. Typed DEPENDS_ON and refutation relationships determine which later claims must be reconsidered. Invalidated supporting claims reopen affected obligations.

A strict obligation discharge requires a valid exact claim and a matching PROVES link. Candidate acceptance checks obligation closure, a unique goal root, current target binding, exact evidence grades, and artifact authority. Completion additionally requires passing final reviews bound to that candidate, assigned to distinct sessions that did not produce it.

Artifact verification can also be withdrawn. Current evidence authority is checked again at candidate admission and completion, and relevant withdrawal history changes the candidate hash so an old review cannot silently authorize a changed candidate. Each result follows the review standard for its domain: proof, computational reconstruction, or experiment.

The resulting record supports outputs at every scale: a useful reduction, an exact counterexample, a computational certificate, an audited partial result, or a complete proof assembled from the work. Catenation’s research campaign proved Nivat’s conjecture, open since 1997, and the proof has been independently verified by researchers in symbolic dynamics. Explore the Nivat case study.

Compute: NCShare, MIT ORCD, and exact replay

Catenation’s compute tooling spans NCShare and MIT ORCD (Engaging). Slurm supplies bounded allocations for research jobs; the biology cluster tools maintain a heartbeat registry of model endpoints, atomic campaign checkpoints, and resumable work. Durable state is kept separate from replaceable model weights and transient compute.

The ORCD mathematics offload path accepts target-bound research and falsification tasks. Returned artifacts retain task hashes and target identity, then pass through independent revalidation before incorporation into the research ledger.

The original fleet recordings ran isolated native sessions and Python kernels on NCShare CPU allocations with authenticated Astra calls. The expanded biology teams use a local open-weight 27B model, served from shared H200-backed NCShare hardware, through a bounded four-call queue. Both preserve the actual model identity and recorded session state. MIT ORCD is an available compute workflow; these particular recordings were made on NCShare.

Scientific tools and inspectable intermediate artifacts

Python functions and callable skills provide a common execution surface for file inspection, literature retrieval, data transformations, and scientific code. The supplied runtime includes arXiv and bioRxiv retrieval, PubMed tooling, H5AD source inspection, and computational-biology skills. Each campaign configures its packages, services, and data for the research question. Each tool return can be kept as a source record, script, calculation, or intermediate artifact for later inspection.

Flexible IPython exploration is distinct from proof-critical computation. The typed broker accepts bounded operations over exact inputs, including rational expression trees, polynomial identities, factorization, characteristic polynomials, Gröbner bases, and specialized random-walk calculations.

Python/SymPy and Wolfram workers can run the same semantic request. The bundle records engine versions, exact inputs and outputs, worker scripts, replay comparison, timing, and file hashes. A semantic hash identifies the mathematical request separately from its execution metadata.

The computation record links each calculation to its interpreted claim and review, making its relationship to the research target explicit.

Formal proof tools

Optional Lean packaging and smoke-check support let teams use formal proof assistants as external checkers. The typed computation broker handles Python and Wolfram operations. Claim-specific review connects checker outputs and computational evidence to the argument they support.

Durable execution and recovery

The Rust interface uses Tokio for asynchronous coordination and Ratatui/Crossterm for the terminal. A daemon owns resident sessions and provider calls. The viewer loads the selected root or child transcript rather than scanning all transcripts on every refresh.

Persistent goals, bounded autonomous continuations, scheduled prompts, heartbeats, agent messages, and compaction support long-running work. Resident research sessions can continue after the terminal closes. A replacement agent can reconstruct the current target and evidence from the ledger.

The recovery guardian uses consistent SQLite backups, integrity checks, complete transcript capture, content-addressed workspace snapshots, and artifact hash verification. Health reports track runtime operations, while the evidence ledger tracks scientific claims and reviews.

The programmable kernel runs with its worker’s operating-system permissions. Each deployment configures the host environment and access to its research tools and data.

Mathematics: the Kunz pair-index campaign

The current capture focuses on a standalone lattice-combinatorics question: under the precise MAX, genuine hidden-contact, and all-five full-complement fixedness hypotheses for an actual strict cyclic staircase, must the selected pair normals generate the full relation lattice?

The capture explores independent approaches to the standalone pair-index question, under the exact hypotheses recorded in its campaign brief.

Recorded sessions, runtime counts, and thread selections let readers follow the captured work. Mathematical results proceed through reconstruction and review in the research ledger.

Computational biology

The local portfolio contains 30 compiled campaign specifications. The gallery opens actual terminal captures for individual campaigns. Launch audits establish the estimand, study design, source requirements, and validation criteria for each campaign.

The biology harness adds identification-specific grades and four central failure modes: triviality, vacuity, leakage, and post-hoc drift. It can check exact identified sets, LP certificates, sign-robustness radii, contamination bounds, monotone-link invariance, holdout leakage, vacuity, and structured permutation nulls.

The biology ledger connects supporting claims to independent reviews and grades results by their supporting evidence. It distinguishes held-out replication, symbolic identities, and proposed mechanisms so readers can inspect the basis of each finding.

Product directions

Foundation-model improvements strengthen the AI agents while Catenation preserves the working environment, evidence, and continuity around them.

The Mantis integration

Mantis Discovery pilots a focused Catenation integration with Mantis in the MIT CSAIL ecosystem. Explore Mantis Discovery ↗

Source and capture provenance

Implementation descriptions were checked against the current mathematics and biology source trees, the supplied Mantis Forge 0.7.1 runnable JavaScript/Python implementation, and the preserved recording evidence.

Code examples use the runtime’s Python APIs. Recorded-run counts and tested-binary identity are documented in the evaluation record.

The research material draws on the Kunz campaign brief, the biology broker and ledger, and the compiled campaign specifications. Public captures connect these mechanisms to actual research sessions.