The structural ideas
behind Eigenius.
This section is for readers who want to understand the framework without committing to learning the platform. What a typed knowledge graph is, why four warrant categories instead of one accountability surface, and what changes when scientific reasoning becomes machine-checkable. If you want to try the platform, head to Get started or Docs instead.
Why are coding agents great
and reasoning agents not?
AI coding agents are unreasonably good because a compiler, a type-checker, and a test suite give them a feedback loop they cannot fake. AI reasoning agents, by contrast, produce prose that nobody mechanically checks — so brilliance and hallucination look identical at the surface. The video below frames the move: build a feedback loop for AI thought out of typed chain commits the kernel can verify.
Every claim — human or AI —
lands in one of four categories.
Three warrant kinds are mechanical — an instrument run, a deterministic computation, or a formal proof — and can be independently re-executed by anyone with read access. The fourth carries an authoritative warrant: a named declarer is on record, and the citation chain is examinable. The distinction is what an AI agent must declare when it commits a claim, and what stops a hallucination from masquerading as a mechanical derivation.
Raw measured data with unbroken instrument provenance.
Example: Six raw IC₅₀ readings from a Kinase-Glo plate run.
Outputs of deterministic computation, rerunnable byte-identically.
Example: A t-statistic and p-value the statistics institution emitted.
Claim accepted by a machine-checked mathematical proof.
Example: A Lean-verified regulatory primary-endpoint result.
Asserted by a named human, organisation, or policy document.
Example: A 100 nM threshold cited from a methodology document.
The four categories are peers, not a hierarchy. The chain doesn't prevent an AI from declaring something false — but it does prevent it from passing a declaration off as a mechanical warrant.
Three deeper concepts.
The declarative first move in crossing between domains.
- Formulate the entities and propositions of a domain
- State implications that link them to a neighbouring vocabulary
- Citable, refutable, chain-resident — translation as data
How runtimes cooperate without sharing a language.
- Goguen–Burstall institutions as the platform's modularity surface
- Comorphisms: typed translations between runtime boundaries
- How institutions lift domain bridges into live computation
The modal calculus behind the warrant taxonomy.
- Artemov's justification logic, chain-instantiated
- JustifiedBy as a typed inductive over evidence
- For the academically curious — coming soon
From idea to a worked example.
When you're ready to see all of this end-to-end in a real workflow, the drug-screening example walks the chain from raw IC₅₀ plate readings to the final designation. Five chain commits, three warrant kinds, one domain bridge, one reasoning certificate — everything type-checked at commit time.