Derivation
Show the derivation
Connect claims to the arguments, sources, and exact computations behind them.
Back to the homepage
Architecture
Inside the research harness.
How Catenation programs context, delegates to AI agents, and carries evidence forward, with the recorded campaigns open to inspect.
The harness
Six mechanisms, step by step.
Program the context and delegate through code. Refine the working environment while the evidence carries forward.
The context is something the agent can program.
The model writes Python to inspect sources, call tools, and work with intermediate objects. The kernel retains those objects; selected results return to the model.
External research state
- Papers + source filesread, inspect, transform
- SOTA Context Maplong-context orientation cache
- Knowledge BaseKnowledge Graph / Ontology
- Evidence ledgerretrieve exact dependencies
Large working material stays outside the prompt. The agent chooses what to inspect.
Turn 1 · select the materialSame kernel
01from mantis_forge import ctx02 03sources = await ctx.search(04 "boundary cases", limit=405)06 07# inspect exact source records08source_map = await ctx.cartography()Out
Selected source records + their relationships
Retained namespace
sourcesselected recordsnewsource_mapnodes + typed edgesnew
Model window
Instructions + selected context + tool results
Python state persists across turns and compaction; kernel failure has a separate recovery path.
Campaign gallery
Open a research campaign.
Read the actual threads, tool outputs, and saved work. Each domain brings its own standard of evidence.
Watch the fleet filmB01 / computational biology
When is a CRISPR lineage recorder a clock?
- Captured source audit and review
- Astra
- 2026-09-21
On a small fixed tree, derive the exact feasible interval under site-rate bounds and one dated anchor; then apply the same code to one processed ConvexML tree using rate bounds estimated from held-out sites. The decisive output is whether any internal node remains materially narrower than [0,T].
Campaign notesWhy it matters
Leave the field with more than an answer.
A useful discovery leaves a method someone else can understand, challenge, and reuse. Catenation keeps the arguments, computations, failed approaches, and dependencies that led to a result, so the intermediate work becomes scientific insight and reusable procedural knowledge.
Obstruction
Keep the obstruction
A counterexample records why an approach fails, so another agent can start beyond it.
Method
Improve the method
Carry useful techniques into prompts, skills, memory, and the next campaign.
The transfer test. With the record, a researcher should solve a related problem, explain a necessary assumption, or repair a broken argument better than with the paper or transcript alone.
Research record
Inside the Nivat campaign.
Catenation’s research campaign proved Nivat’s conjecture, open for 29 years. Inspect the original agent work, computations, refuted approaches, and the resulting argument.
Independently verified by researchers in symbolic dynamics
Read the proof Lean formalization: the full proof, machine-checkedThe question
Does limited local variety force global order?
Imagine sliding a rectangular window over an infinite tiled floor. If it reveals no more distinct patterns than the window contains tiles, must the entire floor repeat in some direction?
First posed in 1997, Nivat’s conjecture became a landmark problem in two-dimensional symbolic dynamics and combinatorics on words: the mathematics of patterns and repetition.
The statement Catenation proved
A finite-alphabet configuration with at most k × n distinct patterns of size k × n has a nonzero period.
Example: a 3 × 2 window slides over a periodic tiled floor. It finds five distinct patterns, no more than its six tiles, and the floor repeats along one direction.
- Approach families
- 11
- Original agent histories
- 7
- Refuted shortcuts retained
- 8
- Claims in the preserved ledger
- 46
Choose a part of the argument, then follow its prerequisites.
Loading the preserved dependency map…
The routes that changed the argument.
The closing route combines annihilator algebra, directional pattern counting, and defect geometry. The research record preserves the calculations and reviews behind each revision.
Exact example
When fewer walls meant more patterns
An exact seven-to-five-wall example increased the number of 2 × 2 patterns from 15 to 16. Deleting a canceling pair was not a valid shortcut.
Counterexample
A sharper counting argument
A counterexample had no rare 2 × 2 patterns but still had a nonzero affine deficit. The closing route instead uses quadratic observables on the same pattern set.
Review
Review that strengthened the argument
Review identified a residual step to resolve. The corrected argument passed two final reviews, and the proof was then independently verified.
The campaign’s full research record, preserved for inspection. The explorer traces 20 connected claims and 25 prerequisite relationships from the original proof.