Eigenius：具备认知分层与制度中介推理的类型化知识图谱 DBMS

View PDF HTML (experimental)

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 whose metatheory is mechanized in Lean 4: a dependent type theory (EigenTT) separating confluent conversion from ontology subsumption and keeping proof irrelevance axiomatic so distinct warrants remain inspectable; proof-calculus institutions acting as strongly typed integration boundaries; and a content-addressed immutable storage layer. Epistemic status (declared/observed/derived/verified) forms a bounded lattice over a justification logic enforced at commit. Cross-system comorphisms carry explicit axiom policies (Adopt, Discharge, Relativize), transport witnesses at commit, and materialize outputs into the graph, while EigenQL provides a Grothendieck query view across all hosted logics and shared on-chain IRs collapse multi-system translations to identity. Pairing empirical justification logic with an in-process Lean 4 term checker, an end-to-end recomputation of a published Nature study from pinned data discharges all 52 derived conclusions and surfaces four machine-checked discrepancies in the original study.

Comments:	Minor corrections to the previous version of the manuscript
Subjects:	Databases (cs.DB); Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO)
Cite as:	arXiv:2608.04457 [cs.DB]
	(or arXiv:2608.04457v3 [cs.DB] for this version)
	https://doi.org/10.48550/arXiv.2608.04457 arXiv-issued DOI via DataCite

Submission history

From: Hans-Martin Will [view email]
[v1] Wed, 5 Aug 2026 05:28:22 UTC (17 KB)
[v2] Tue, 18 Aug 2026 15:52:48 UTC (17 KB)
[v3] Thu, 5 Nov 2026 16:02:06 UTC (19 KB)