Proof checking
Proof kernel
The small part of a proof system that checks declarations and proof terms.
Definition
Proof kernel
A proof kernel checks that terms are well typed and that theorem terms have their declared proposition types.
Elaboration and tactics may perform complex search outside the kernel. The final declaration enters the environment only after the kernel accepts it.
01
Example
The Axeyum Kernel checks selected Lean-core terms in Rust without running Lean as its checker.
02
Important distinction
A kernel is not an interactive proof assistant. It may have no editor, tactic language, or goal display.
After reading this article, you should be able to
- Define Proof kernel in the sense used on this site.
- Separate the kernel's checking work from elaboration and tactic search.