发表机构
The Eigenius Project; Docimion（Eigenius项目; Docimion）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
Eigenius是一款开源类型化知识图DBMS，通过耦合类型系统等实现数据溯源不变，统一科学认识论，在Nature研究复现中验证了52个结论并发现4处差异。
AI 中文摘要
随着“AI科学家”通过模型上下文协议（MCP）推动研究，依赖临时脚本的系统将失效。状态化、相互关联证据的庞大规模需要基于专用数据库架构的机器可遍历保证。Eigenius是一款开源的类型化知识图数据库管理系统，建立在一个核心前提之上：回答审计问题（“你知道什么，你的保证是什么？”）需要一个统一内核。通过将类型系统、存储引擎和集成协议紧密耦合，Eigenius将数据溯源转变为结构不变量，而非跨子系统边界重构的属性。该内核基于三大支柱：贯穿核心的依赖类型理论、作为强类型集成边界的机构（institutions），以及内容寻址的不可变存储层。在此基础上，认知状态（声明/观察/推导/验证）被强制为严格的提交时不变量。跨系统转换（共态映射，comorphisms）在提交时被检查，并作为持久的一等资源直接物化到图中。为消除O(N²)多存储瓶颈，共享链上中间表示（IR）将多系统转换简化为恒等操作。关键的是，该架构统一了科学认识论的两个领域：它将辩护逻辑用于经验科学，同时嵌入快速的进程内项检查器，以在无IPC开销的情况下安全评估形式化数学证明（通过Lean 4）。在一项从脆弱脚本到物化证据图的已发表Nature研究的端到端重新计算中，所有52个推导结论均来自固定数据，发现了原始研究中的4个机器检查差异。
英文摘要
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.
CommentsMinor corrections to the previous version of the manuscript
