Eigenius: A Theoretical Framework for Typed Knowledge Bases for Mathematical Proofs

When Proofs Are No Longer "Anonymous": The Challenge of Knowledge Persistence for Type Theory

In the fields of mathematical formalization and program verification, the design goal of type theory is usually quite pure: it only cares whether a proposition holds. Proof irrelevance, as a conversion rule, erases at the kernel level the information of "how this proposition was established." In other words, two different proof terms, as long as they prove the same proposition, are considered equal during conversion—the derivation process, the participation of external tools, and the assumptions relied upon all disappear.

But a persistent knowledge store cannot work this way. It needs to record: who established this assertion, through which derivation or which external tool, and under what assumptions it holds. This is precisely the problem that the book Typed Knowledge over Constructive Institutions aims to solve. The book proposes the theory of Eigenius—a typed knowledge store built on constructive institutions—and develops its metatheory starting from this requirement.

Kernel Design: Proof Irrelevance as an Axiom Rather Than a Conversion Rule

The kernel of Eigenius is a dependent type theory that includes cumulative universes, an impredicative universe of propositions, inductive families, and an intensional identity type.

The key design is that proof irrelevance is stipulated as an axiom with an explicit witness, rather than as a conversion rule. This means that although two proofs of a proposition can be proven equal, they remain distinct terms—the kernel can distinguish them. This change may seem subtle, but it preserves room for tracking the provenance of evidence.

Definitional equality is characterized by joinability under an orthogonal rewriting system. This system is confluent, injective on type formers, and decidable via a type-free test. In addition, an independent subsumption judgment handles universe cumulativity, codomain-covariant function types, and declared class inclusions.

Proof irrelevance has two common treatments in type theory: as a conversion rule, the type checker directly ignores the internal structure of two proof terms when deciding whether they are equal, treating them as interchangeable as long as they prove the same proposition; as an axiom, one must explicitly declare "if p and q both prove proposition A, then p = q," and the proof of this equality is itself a term that needs to be constructed and tracked. Eigenius chooses the latter, meaning that proof equality is no longer an implicit side effect of type checking, but an assertion with a witness. This is analogous to changing, in a database, "two records point to the same entity" from hard-coded deduplication logic into an auditable merge record.

An orthogonal rewriting system is a class of rewriting systems that satisfies left-linearity (each variable appears at most once on the left-hand side) and has no critical pairs; its confluence is directly guaranteed by orthogonality, without additional verification. Eigenius uses joinability to characterize definitional equality: two terms are definitionally equal if and only if they can be rewritten to a common term. Because the system is orthogonal and decidable, the type checker can decide equality via a type-free test without relying on complex reduction strategies.

Metatheory: Consistency, Evidence Tracking, and Institutional Organization

The author builds the metatheory of Eigenius at multiple levels. First, consistency of the system is proven via a set-theoretic model. Second, a justification logic is developed on top of kernel propositions to track evidence and support relations.

The environment is organized as an institution; store extensions become signature morphisms, and external verdicts enter via comorphisms. This design allows the verdicts of external tools—theorem provers, computation engines, or other verification services—to flow into the knowledge base in a controlled manner.

On this basis, the author also formalizes a typed knowledge-graph theory comprising records, classes, and refinements. The correctness of conversion, normalization by evaluation, and bidirectional type checking with respect to termination is also proven.

It is worth noting that the work comes with a Lean 4 formalization, meaning that the core conclusions in the book have been machine-verified, not merely derived on paper.

Justification logic is a refinement of modal logic that replaces "□A" (A is necessary) with "t : A" (term t is a justification of A), where t can be a proof, evidence, or an explicit record of a support relation. Unlike traditional proof logic, justification logic allows tracking the structure of evidence: the same proposition can be supported by different justification terms, and justification terms can be combined and merged. Eigenius develops justification logic on top of kernel propositions precisely to record "who, and by what means" established an assertion, without breaking the axiom of proof irrelevance.

Constructive institutions are a variant of institution theory within constructive type theory. Classical institution theory uses a category-theoretic framework to uniformly describe logical systems: signatures correspond to languages, signature morphisms correspond to language translations, and model functors together with satisfaction relations form the core of an institution. Eigenius models extensions of the knowledge store as signature morphisms and channels the verdicts of external tools (theorem provers, computation engines) in via comorphisms—comorphisms are translations between institutions that preserve satisfaction relations, ensuring that semantics are not lost when external results enter the knowledge base. This design enables the results of heterogeneous verification tools to be integrated in a controlled, traceable manner.

Why This Matters for Knowledge Bases and AI Systems

Although Eigenius's motivation comes from mathematics and program verification, its problem awareness also holds for broader knowledge management scenarios. Current knowledge graphs and databases, when storing assertions, often retain only the "conclusion" while ignoring the complete evidence chain of "who, how, and under what premises" the conclusion was reached. When multiple sources conflict, or when an external tool upgrade causes a conclusion to become invalid, systems lacking evidence records find it difficult to trace and correct.

Eigenius's approach is to build evidence tracking into the type system, so that the knowledge base structurally cannot lose derivation history. This "evidence-first" design offers a theoretical path different from traditional database approaches for knowledge systems that require auditing, provenance, and continuous updating.

Of course, this theory is still at the metatheory construction stage, and there is still a distance to engineering implementation. But its way of combining institution theory, justification logic, and dependent type theory provides a noteworthy framework for constructive knowledge management.

Conclusion

By demoting proof irrelevance to an axiom with a witness, introducing justification logic to track evidence, and organizing knowledge extensions via institutions, Eigenius attempts to solve the problem of evidence preservation for knowledge persistence at the kernel level. The Lean 4 formalization enhances the credibility of the conclusions. For researchers and engineers interested in applications of type theory, formal verification, and knowledge representation, this book provides a rigorously structured reference framework.

One-line Summary

Eigenius demotes proof irrelevance to an axiom with a witness and uses type theory to build evidence tracking into knowledge stores.

Paragraph Summary

The article introduces the Eigenius theory proposed in the book Typed Knowledge over Constructive Institutions: a typed knowledge store framework based on constructive institutions. Its core design is to change proof irrelevance from a conversion rule into an axiom with an explicit witness, so that different proofs of the same proposition remain distinguishable in the kernel, thereby preserving derivation history and evidence provenance. The kernel uses dependent type theory, and definitional equality is characterized by joinability under an orthogonal rewriting system. At the metatheory level, the author proves consistency via a set-theoretic model, develops justification logic to track evidence, and organizes the environment as an institution so that the verdicts of external tools enter the knowledge base via comorphisms. The work comes with a Lean 4 formalization, and the core conclusions are machine-verified. The article argues that this "evidence-first" design has theoretical reference value for knowledge management systems that require auditing, provenance, and continuous updating, but it is still at the metatheory stage.