Axeyum Kernel

Implementation

Axeyum implements a proof kernel in Rust. It checks dependent terms, universes, reduction, definitional equality, inductive declarations, recursors, and the axiom footprint of accepted declarations.

The kernel can check selected material exported from Lean, but Lean is not its runtime. Lean is the principal reference system for the supported term language and import boundary.

• Dependent terms and universe levels
• WHNF and definitional equality
• Inductive types and recursors
• Declaration dependencies and axiom footprints

Rust crates

These crates implement the component or connect its results to another Axeyum checker. Each link opens the crate's source directory.

• axeyum-lean-kernel Independent proof checker
• axeyum-lean-import Untrusted Lean export importer

Reference systems and results

The Lean report states which declarations the Rust kernel checks and which Lean functions it does not provide.

Problems studied with this component

• A BCNF decomposition counterexample Database theory
• The cause of an impossible project deadline Operations research

Current limit