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 · v1
cs.AI cs.LO
TL;DR
Embeds an in-process Lean 4 term checker to safely evaluate formal mathematical proofs within the knowledge-graph DBMS kernel.
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 systems relying on ephemeral scripts cannot provide auditable, provenance-grounded warranties over stateful, interconnected scientific evidence at scale.
Approach
Eigenius is a typed knowledge-graph DBMS coupling a dependent type theory, strongly typed integration boundaries (institutions), and content-addressed immutable storage. Epistemic status is enforced as a commit-time invariant and cross-system translations are checked at commit. It uses justification logic for empirical science and embeds a fast in-process Lean 4 term checker to evaluate formal mathematical proofs without IPC overhead.
Results
In an end-to-end recomputation of a published Nature study, all 52 derived conclusions held from pinned data, surfacing four machine-checked discrepancies in the original study.