Theoria

Theoria is an Elixir-native proof/spec kernel inspired by Lean's trusted-kernel architecture.

The goal is not Lean compatibility. Theoria starts as a small, reliable core for checking proof terms generated by Elixir DSLs, tactics, and domain-specific specification tools. The first target domains are finite data structures, graph algorithms, compiler passes, and static-analysis invariants.

Theoria is intentionally split into a small trusted kernel and future untrusted convenience layers. DSLs and tactics may generate proof terms, but only the kernel can admit checked declarations.

Installation

def deps do
  [
    {:theoria, "~> 0.1.0"}
  ]
end

Design principles

• Keep the trusted kernel small.
• Treat DSLs, macros, tactics, and automation as untrusted proof generators.
• Admit a theorem only after the kernel checks its proof term.
• Use precise Elixir structs and result tuples so the codebase is friendly to Elixir's gradual set-theoretic type direction.
• Grow through tests and proof corpora before adding convenience layers.

See docs/design.md for the current design notes.

Current status

The initial kernel supports:

• universe terms (Type n as Sort n)
• de Bruijn bound variables
• constants
• lambda abstraction
• dependent function types (forall)
• application
• beta reduction
• definitional equality by normalization
• checked constants and definitions in an environment

Example core term

import Theoria.Term

identity_type =
  forall(:a, sort(0),
    forall(:x, bvar(0),
      bvar(1)
    )
  )

identity_proof =
  lam(:a, sort(0),
    lam(:x, bvar(0),
      bvar(0)
    )
  )

:ok = Theoria.Kernel.check(Theoria.new_env(), identity_proof, identity_type)

Quality checks

The repository includes a Reach-style CI alias:

mix ci

It runs compilation with warnings as errors, formatting, Credo, ExDNA, Reach architecture/smell checks, Dialyzer, and tests.

Roadmap

1. Harden the kernel with more normalization, substitution, and negative tests.
2. Add equality and basic logical connectives.
3. Add primitive Bool/Nat/List theories.
4. Add a small Elixir DSL that elaborates to checked core terms.
5. Add finite graph/spec libraries for tools such as Reach.