← 研踪 PaperTrailarXiv:2608.04457 · v3
Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning
首次提交 2026-08-05 13:28
版本更新 2026-11-06 00:02
雷达观测 2026-11-06 12:09
摘要
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.
作者备注：Minor corrections to the previous version of the manuscript
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v3 · 2026-11-06 00:02 · 最新观测版本
Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning
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.
查看此版本解读 →查看此版本原文 ↗