A minimal, self-contained implementation of a Lean 4-style theorem prover kernel in Rust. This repository is built from scratch to illustrate the core foundations of dependent type theory, inductive types, and kernel type checking without the complexity of a full production prover.
-
Dependent Type Theory Core: Dependent function types (
$\Pi$ -types), universe hierarchy, and term representation (src/term.rs). -
Type Checking & Reduction: Type inference (
src/typecheck.rs),$\beta/\delta/\iota$ -reduction (src/reduction.rs), capture-avoiding substitution, and$\alpha$ -equivalence (src/substitution.rs). -
Inductive Types: Support for inductive declarations, strict positivity checking (
src/inductive/positivity.rs), and recursor generation (src/inductive/recursor.rs). -
Minimal DSL (
.leanmini): Custom syntax parser (src/syntax.rs) and CLI runner for verifying.leanminiproof scripts.
The book Implementing an Interactive Theorem Prover from Scratch explains this kernel chapter by chapter, with the real kernel compiled to WebAssembly so every example can be run and edited in the browser. It is published at learn.h5i.dev in English, Japanese, and Simplified Chinese. The built site is the docs/ folder (open it through a local web server, for example python3 -m http.server inside docs, to use the playgrounds); the sources and build script are in docs/book/, and the original paper is in docs/paper/.
Verify the example proofs in the examples/ directory using Cargo:
cargo run -- examples/identity.leanmini
cargo run -- examples/nat-reflexivity.leanmini
cargo run -- examples/zero-add.leanmini
cargo run -- examples/generic-list.leanmini
cargo run -- examples/generic-vec.leanminicargo testSee LICENSE for details.