Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning
Hans-Martin Will, Allen L. Brown, Matthew Fuchs
cs.DB
Aug 5, 2026 · v2
cs.AI cs.LO
TL;DR
Embeds an in-process term checker in a knowledge-graph DBMS to evaluate Lean 4 formal mathematical proofs without inter-process communication overhead.
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.
Problem
AI-driven research workflows that rely on ephemeral scripts cannot provide auditable provenance for large, interconnected bodies of evidence. Answering what a system knows, and on what warranty, requires provenance to be built into the database architecture.
Approach
Eigenius is an open-source typed knowledge-graph DBMS. It combines a dependent type theory, institutions acting as typed integration boundaries, and content-addressed immutable storage. Epistemic status (declared/observed/derived/verified) is enforced as a commit-time invariant, and cross-system comorphisms are checked and stored as first-class graph resources. Empirical claims are handled with justification logic, while an embedded term checker evaluates Lean 4 proofs in-process.
Results
In an end-to-end recomputation of a published Nature study, all 52 derived conclusions held from pinned data. The recomputation surfaced four machine-checked discrepancies in the original study.
