Skip to content
Eigenius

Research

Eigenius sits at the intersection of three traditions. The typed-knowledge-graph machinery descends from the dependently-typed calculi pioneered by Coq, Lean, and Agda; the four-warrant taxonomy is a chain-instantiated form of Artemov’s justification logic; the modular dispatch architecture borrows from Goguen-Burstall institution theory. This section collects the papers that present the framework academically, along with the citation anchors and the recommended reading order for someone coming from each tradition.

Papers

Both papers are in active preparation. Abstracts, manuscripts, and submission details will be posted here as soon as they land at their target venues. In the interim, the worked examples and the concepts cover the same material in narrative form.

How to cite

A formal citation entry will appear here once the papers land at their target venues. In the interim, please cite the GitHub repository with the commit hash you reference; the platform’s content-addressed identifiers make a precise citation straightforward:

@misc{eigenius2026,
  author       = {The Eigenius Authors},
  title        = {Eigenius: a typed knowledge graph for
                  auditable scientific reasoning},
  year         = {2026},
  howpublished = {\url{https://github.com/eigenius/eigenius}},
}

Reading order, by background

While the papers are in preparation, the material is best approached through this site and the repository. By tradition:

From type theory (Coq, Lean, Agda, dependent types): start with the Concepts overview for the chain-instantiation framing; then dip into the design notes in the repository under docs/design/ for the specific extensions to standard dependent type theory that the chain requires (proof-irrelevance in the propositional universe, content-addressed type expressions, the parent-pointer layer chain). The ESL chapter §6 — Resources, types, and the layer is the bridge between the resource graph and the type system.

From justification logic (Artemov, modal calculi): the Justification logic page is the bridge from Artemov’s calculus to the chain-resident form. The four-warrant taxonomy is the chain instantiation; each JustifiedBy constructor in the reasoning institution’s inductive type maps to one of Artemov’s evidence-bearing modalities.

From provenance and FAIR / ALCOA+: the Drug-screening example is the canonical end-to-end illustration. The chain delivers most of the ALCOA+ enumeration structurally; the verifier closes the accurate principle by deterministic re-execution rather than by author attestation. The Science paper, when it lands, will include the full ALCOA+ alignment table.

From AI / ML systems: the Concepts overview frames the chain as the substrate for inspectable AI reasoning. The kernel is “a compiler for AI thought” — agents must produce typed proof terms the type-checker admits; hallucinations either fail to commit or land visibly as Declared artifacts with the agent on record. The Domain bridges page is the most direct illustration of how the type discipline blocks the most common AI failure mode (unjustified cross-vocabulary leaps).