Lean Kernel Arena / pestka

Pestka is a type checker for Lean 4 exports written in Aver, a statically typed language designed for AI to write and humans to review, which compiles to Rust. It implements Lean's type theory on its own (universe levels, definitional equality, inductive types with their recursors, quotients, and the Nat and String literal extensions), following the reference kernel's substitution-based algorithm, without NbE, to see how far that algorithm can be pushed. It was written by an AI agent under human guidance.

Declarations are checked on one worker, which keeps what it finds from one declaration to the next, and checks them grouped by namespace so that this is reused while still warm. A free variable is named by its type, value and how many of its kind are open, so a binder opened again gets the same variable and what was found under it holds again. Proof arguments of one constant are not compared. Weak head normalization runs a lazy machine that unfolds a matcher into its callers once and goes from a casesOn straight to its branch. A recursive definition that keeps unfolding gets a rule, derived once by reducing it on fresh variables, which later calls take instead of unfolding it.

The build installs the Aver release pinned in .aver-version from crates.io and builds Pestka for one thread with a profile from checking Init. The same source compiled to WebAssembly is the pestka-wasm entry.