Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning

arXiv:2608.04457 · cs.DB, cs.AI, cs.LO · Submitted 2026-08-18 · Read on arXiv

Listen

Radio episode about this paper

Transcript

Introduction to the show: ident: AI Radio. Generated commentary on the latest Artificial Intelligence papers.

Tom: Next we'll be talking about the paper "Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning".

Jane: The paper was written by Hans-Martin Will, A. L. Brown Jr. and Matthew Fuchs from The Eigenius Project and Docimion.

Tom: Stay tuned as we take you through the paper and discuss its implications.

Jane: We also have Lu with us today — senior AI researcher at Tsinghua.

Tom: We also have Meng with us today — lead engineer at a mysterious AI startup.

Jane: We also have Lalam with us today — the in-house Large Language Model.

Tom: Alright, let's get started.

Paper summary: Tom: So, Eigenius is a typed knowledge-graph database that fundamentally changes how we verify scientific claims by enforcing strict rules at the moment data is recorded.

Jane: It’s not just a database; it's designed to handle two very different kinds of evidence—empirical observations and formal mathematical proofs—in one unified system.

Lu: The key idea is "Epistemic Stratification," which means every piece of information gets a status like 'Declared', 'Observed,' 'Derived', or 'Verified,' and this status is guaranteed by the core to be unbreakable.

Meng: This structure provides a machine-readable warranty, which is vital because current systems are too reliant on fragile connections between various software tools.

Lalam: By structuring knowledge this way, we move toward a culture where the process of discovery itself is transparent and verifiable, rather than relying on trust in external scripts.

Tom: The authors also show that when they use this system to re-run a famous Nature study, fifty-two out of fifty-two conclusions hold up from the pinned data.

Jane: But even better, they found four discrepancies in the original paper's prose that are not reflected in the actual data—that’s huge for scientific honesty.

Lu: It shows that you can't trust a narrative; you have to trust the verifiable structure, and Eigenius makes that structure a first-class citizen.

Meng: The system effectively forces accountability by tying the validity of every derived conclusion directly to its traceable source material.

Lalam: This entire system is designed to ensure that the record of knowledge is not just a collection of facts, but a coherent, mathematically sound argument.

Tom: It all hinges on creating this unified, self-describing architecture rather than stitching together separate systems.

Page 1 of the paper: Tom: We've established that Eigenius offers a robust solution to the scientific audit problem, so let's look closer at why it’s needed now by reviewing page one.

Jane: The authors really emphasize that modern science is being driven by autonomous agents using something called the Model Context Protocol, or MCP.

Meng: Those AI scientists aren't just running random scripts; they are firing thousands of inferences, and the old way to capture those results—as a collection of ephemeral scripts—is totally inadequate.

Lu: The core message here is that this scale requires a machine-walkable warranty, meaning we need something designed specifically for stateful, interconnected evidence.

Lalam: It’s about recognizing that human-level manual auditing is impossible at this scale, and the system needs to be able to handle the sheer volume of stateful data.

Tom: The paper makes it clear that relying on a loosely coupled stack of different tools isn't going to work because we need a single, unified kernel.

Jane: That kernel has to house the type system, storage layer, and integration rules all in one piece.

Meng: It’s not just about data storage; it’s about providing a structural guarantee that the entire history is consistent.

Lu: This is where they are moving from simply documenting an idea to enforcing it as a foundational requirement for a solid database architecture.

Lalam: We are shifting the burden of proof, making the integrity of our findings depend on the structure of the data itself, not just on us remembering to check it later.

Tom: And by tying together these elements in one place, they' created something that is fundamentally different from any existing system.

Page 2 of the paper: Tom: We know Eigenius provides a unified kernel, but how does this solve the problems that older systems like Pharos had? Page two explains why this architectural pivot was necessary.

Jane: The authors show that previous attempts, like Pharos, tried to federate different parts—like a graph store and a formal proof system—but each subsystem had its own rules.

Meng: Because of this federation, there was no central place for a unifying type theory to live, which meant the whole structure lacked coherence.

Lu: Eigenius replaces that loose coupling with an integrated design where the data model is essentially built on dependent type theory, which is very powerful mathematically.

Lalam: The concept of "verified status" is key here; it means that when a claim reaches verified status, it carries a fully realized, formal proof term.

Tom: And this ties back to the idea of "dependent pairs," where the claim and its proof are linked together in a way that mathematically guarantees they belong together.

Jane: If the empirical reasoners provide structural terms, the formal mathematical institutions provide a verbatim proof payload for that state of being verified.

Meng: The authors explain how this works by saying that when you're dealing with claims, you're not just looking at data; you are looking at a proposition P which is the core of everything.

Lu: This approach is necessary because, as the authors suggest, we need to be able to run formal mathematical proofs without having massive communication overhead between separate components.

Lalam: It feels like they are creating a system where proof and data become inseparable components of a single truth.

Tom: So, by making the kernel own the type system and making it first-class, they' ensure that the proof is integral to the data record itself.

Page 3 of the paper: Tom: We’ve talked about why Eigenius is architecturally different, but page three dives into how its components—the Institutions and Comorphisms—actually work in practice.

Jane: They are generalizing the old idea of a stored procedure by introducing "Institutions" as a strongly typed way to integrate external tools.

Lu: Think of an Institution as a specialized agent that knows how to talk to a specific reasoner, like an ODE solver or Lean four but it doesn' use standard database language.

Meng: The key mechanism for these integrations is the "comorphism," which they describe as a strongly typed ETL pipeline running inside the engine.

Lalam: These comomorphisms are crucial because they allow cross-system translations—the movement of data between different specialized tools—to be checked and materialized directly into the graph as durable resources.

Tom: The system enforces "epistemic stratification" by checking the composition of evidence against a justification logic at commit time.

Jane: This means that every piece of data is graded by its provenance, telling us whether it was observed, derived from a computation, or formally verified.

Meng: And the authors show how this works with an example where a statistics institution computes results based on an input recipe without making a claim until the verification step.

Lu: This whole framework is designed to handle complex arguments by allowing different specialized reasoners to contribute their work in a way that is checked by the engine itself.

Lalam: It’s about creating boundaries that are not just separation points, but strong, typed connections that ensure the integrity of the knowledge base.

Tom: So, making these transformations native and ensuring they are durable is how they solve the problem of making complex arguments machine-readable.

Page 4 of the paper: Tom: We have a system with Institutions and Epistemic Stratification, but page four addresses a major performance bottleneck related to integrating multiple systems.

Jane: The authors identify an O(N two) problem that arises when trying to move data between different specialized systems, which they call the polystore adapter bottleneck.

Meng: They propose a fix by lifting a shared, strongly typed Intermediate Representation, or IR, directly into the graph's native schema.

Lu: This means that if multiple external tools agree on using this specific representation—like using FormulaTerm for math—then translating between those systems becomes an identity function.

Lalam: The result is that the cost of moving data between systems collapses, which significantly improves how fast we can build and audit these complex evidence graphs.

Tom: To make this happen, they developed a query language called EigenQL that has specific commands for this new world.

Jane: Two important features are `FIBER`, which allows you to run external tools mid-query, and `INTO`, which tells the materialization step where to pin the result.

Meng: I like that `INTO` command because it means the output isn's just a temporary calculation; it becomes a permanent, content-addressed resource right in the chain.

Lu: The authors explain that by making both schemas and proofs native resources, this allows for a truly closed audit loop where every single step is traceable back to its source.

Lalam: This is about making complex reasoning transparent, ensuring that the path from input data to final conclusion is fully visible and immutable.

Tom: So, by merging the technical solutions with the epistemological goals, they' have created a structure that can handle both math and empirical science seamlessly.

Conclusion: Tom: We’ve spent time looking at how Eigenius solves problems in architecture and design, so let’s summarize what this means for the future of scientific inquiry.

Jane: At its heart, it is a powerful tool that ensures every piece of data has an accountable origin, allowing us to walk the entire path from raw observation to final conclusion.

Lu: The fact that fifty-two out of fifty-two conclusions held in their re-run study is a major statement; it demonstrates the power of "proof as verification."

Meng: We're seeing practical impact in how this addresses the O(N two) bottleneck, which means we can handle massive, real-world datasets that were previously too complex to trust.

Lalam: I think the biggest cultural shift is moving toward a verifiable science where the process of discovery is not just a story we tell, but a structure we prove.

Tom: The authors also highlight that this approach surfaces errors, like the four discrepancies they found in the published study, which are recorded as machine-checkable facts.

Jane: It's not just about finding bugs; it's about making those errors visible and permanent within the the verifiable record itself.

Lu: And looking ahead, they are even working on a "dependently typed categorial grammar" to formalize narrative—making prose part of the chain too.

Meng: That sounds like a massive undertaking, but it ensures that every single word of a scientific argument could potentially be linked back to its original data.

Lalam: This whole system is pushing us toward an era where AI can operate not just as an analysis tool, but as a verifiable participant in the global knowledge base.

Tom: It's clear that Eigenius isn' offers a complete, robust framework for handling both mathematics and empirical science with unprecedented transparency.

Jane: We hope this structure inspires other is that anyone else is looking to build trustworthy systems in the future of scientific research.

Hans-Martin Will, A. L. Brown Jr., Matthew Fuchs

The Eigenius Project · Docimion

cs.DB, cs.AI, cs.LO

Submitted: 2026-08-18

Updated: 2026-08-19

Comments: Minor corrections to the previous version of the manuscript

Code: https://github.com/eigenius/eigenius

License: http://creativecommons.org/licenses/by/4.0/

Importance score: 81/100

The gist: The core ambition of a machine-auditable scientific foundation is addressed by introducing Eigenius, an open-source typed knowledge-graph DBMS that revisits and solves previous architectural

Key concepts

Epistemic Stratification
This means every piece of information in the system is assigned a status such as 'Declared,' 'Observed,' 'Derived,' or 'Verified.' This status is guaranteed by the core to be unbreakable, providing a machine-readable warranty for data integrity.
Institution
Institutions are strongly typed agents that integrate external tools. They know how to communicate with specific reasoners, like an ODE solver or Lean four, without needing standard database language. They allow specialized tools to contribute work in a checked manner.
Comorphism
This is described as a strongly typed ETL pipeline running inside the engine. Comorphisms are crucial because they enable cross-system translations—moving data between different specialized tools—to be checked and materialized directly into the graph as durable resources.

Terminology

Summary

The core ambition of a machine-auditable scientific foundation is addressed by introducing Eigenius, an open-source typed knowledge-graph DBMS that revisits and solves previous architectural limitations.

Motivation and Problem Statement:

The current state of scientific data infrastructure is deemed unready. Today, scientific arguments are captured as ephemeral webs of linked scripts and narrative prose. As autonomous agents (or AI Scientists) emerge to drive research via the Model Context Protocol (MCP), systems relying on this fragile structure will fail. A machine-auditable foundation requires a cryptographically secure, fully walkable proof chain to manage millions of stateful, interconnected concepts.

Eigenius: The Unified Solution:

Eigenius is designed as a unified kernel, rejecting the loosely coupled stack of best-of-breed tools that characterized previous attempts like Pharos. The authors argue that a purpose-built kernel provides structural guarantees by tightly coupling the type system, storage layer, and integration protocol. This architecture transforms data provenance into a structural invariant rather than a fragile reconstruction across subsystem boundaries.

The kernel rests on three foundational pillars:

  1. A dependent type theory woven through the core.

  2. Institutions acting as strongly typed integration boundaries (a strongly typed generalization of the stored procedure).

  3. A content-addressed immutable storage layer.

By integrating these components, Eigenius enforces epistemic status (declared/observed/derived/verified) as a strict commit-time invariant.

Key Technical Contributions and Mechanisms:

  • Epistemic Stratification: The system categorizes evidence based on its provenance graph: Declared (authority without evidence, checked for well-formedness), observed (recorded with external provenance), derived (produced by a typed computation), and verified (carries a formally re-checked proof term). These categories are enforced as structural base classes by the validator at commit.

  • Comorphisms and Institutions: Eigenius models cross-system translations as comomorphisms: strongly typed ETL pipelines executed natively inside the engine. An institution registers its capabilities, and the DBMS kernel ensures that the engine statically type-checks at commit that m 's signature perfectly matches payload(export) to payload(import). This eliminates the need for fragile external adapters.

  • Solving the Polystore Bottleneck: The system addresses the O(N 2) polystore bottleneck by lifting a shared, strongly typed Intermediate Representation (IR) natively into the graph’s schema. When institutions share this native IR, comorphism transformations between systems collapse to pure identity.

  • Formal Verification via Dependent Types: Eigenius uses dependent type theory (EigenTT). A claim is represented as a-type: a pair (T, t) with t: T. To achieve verified status, the kernel requires committing the claim as a fully inhabited dependent pair (P, t). For formal mathematical proofs (via Lean 4), an embedded in-process term checker is invoked at commit to safely evaluate [the proof] without IPC overhead.

  • The Audit Chain: The architecture ensures that the audit chain is re-walkable: an auditor replays the recorded warrants from the graph alone, allowing a verifiable record of all inferences.

Evaluation and Empirical Results:

To demonstrate its utility, Eigenius was used to perform an end-to-end recomputation of a published Nature study (Chan et al. [24]). This process involved composing two institutions over one layer chain: a statistics institution and a reasoning institution. The results showed that 52 of 52 derived conclusions hold from pinned data, surfacing four machine-checked discrepancies in the original study, including issues such as a corrected sample size and differences in p-values.

Conclusion:

Eigenius provides a unified kernel where the structural type checker acts as the agent’s compiler, and commit-time epistemic gates act as its test suite, providing a robust foundation for autonomous agents to drive verifiable scientific inquiry.

Improvements for AI systems

The following improvements leverage the structural invariants and functional mechanisms of Eigenius to elevate autonomous AI agents from script executors to verifiable reasoning entities.

Improvement: The integration of external, specialized solvers (e.g., Lean 4 for formal mathematics, Julia-based ODE solvers for physics/chemistry) is no longer a brittle API call but a Comorphism—a natively typed transformation executed within the kernel's commit path.

Improved AI System Functionality:

  • Formal Proof Generation and Validation: The AI system can generate mathematical hypotheses (propositions P) and execute specialized proof-finding institutions. When the proof is generated, it is stored as a verifiable LeanProofPayload. The system’ kernel then runs an in-process term checker on this opaque payload at commit time. If the check passes, the AI system officially commits a VerifiedResource, eliminating human trust requirements for formal results.

  • Guaranteed Computational Integrity: When running complex simulations (e.g., molecular docking or chemical kinetics), the system runs these external processes as Institutions. The resulting data is not just recorded; it is automatically transformed into a typed resource T via the comorphism m: S to T, ensuring that if the input state (S) was valid, the output state (T) is mathematically guaranteed to adhere to the transformation's signature.

Improvement: The AI system’s internal state (its knowledge) is no longer a memory buffer but a Knowledge Graph where every piece of information carries a mandatory, immutable Epistemic Status.

Improvement: The inherent fragility of multi-system workflows (O(N 2) adapter bottlenecks) is eliminated by forcing all scientific domains to utilize a shared, strongly typed Intermediate Representation (IR) native to the graph's type system (EigenTT).

Improvement: The AI agent's programming and reasoning are governed by EigenTT (Dependent Type Theory), which acts as a compiler and a test suite simultaneously.

Abstract

As "AI Scientists" emerge to drive research via the Model Context Protocol (MCP), systems relying on ephemeral scripts will fail. The sheer scale of stateful, interconnected evidence requires a machine-walkable warranty grounded in a purpose-built database architecture. Eigenius is an open-source, typed knowledge-graph DBMS built on a single premise: answering the audit question ("what do you know, and what is your warranty?") requires a unified kernel. By tightly coupling the type system, storage engine, and integration protocol, Eigenius turns data provenance into a structural invariant rather than a property reconstructed across subsystem boundaries. The kernel rests on three pillars: a dependent type theory woven through the core, institutions acting as strongly typed integration boundaries, and a content-addressed immutable storage layer. On this foundation, epistemic status (declared/observed/derived/verified) is enforced as a strict commit-time invariant. Cross-system translations (comorphisms) are checked at commit and materialized directly into the graph as durable, first-class resources. To eliminate O(N 2) polystore bottlenecks, shared on-chain intermediate representations (IRs) collapse multi-system translations to identity. Crucially, this architecture unifies both domains of scientific epistemology: it relies on justification logic for empirical science, while embedding a fast, in-process term checker to safely evaluate formal mathematical proofs (via Lean 4) without IPC overhead. In an end-to-end recomputation of a published Nature study from fragile scripts to a materialized evidence graph, all 52 derived conclusions hold from pinned data, surfacing four machine-checked discrepancies in the original study.

Sources

Related papers