arXiv cs.AI· Hans-Martin Will, Allen L. Brown Jr., Matthew Fuchs·· 11 小时前AI 评分31
Eigenius：带认知分层与制度中介推理的类型化知识图谱 DBMS
Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning
AI 导读
Eigenius 是一个开源类型化知识图谱 DBMS，将类型系统、存储引擎与集成协议耦合在同一内核中，使数据溯源成为结构性不变量。其内核基于 Lean 4 机械化元理论，包含分离转换与本体归摄的依值类型理论 EigenTT、作为强类型集成边界的证明演算制度，以及内容寻址的不可变存储层。
正文 · 原文
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)
来源：arXiv cs.AI · arxiv.org