Introduction
We will consider Lean's type theory as a language for writing formal proofs. The part of Lean that enforces the rules of the type theory is called the kernel. The type theory is built from few primitives, enabling the kernel to remain small. From a foundational perspective, trusting Lean means trusting the correctness of this small kernel.
Expressed directly in kernel primitives, even simple proofs can be very verbose. The user-facing surface syntax is more implicit and compressed. Elaboration translates surface syntax into primitives, filling in the implicit pieces. Tactics are an especially powerful form of this compression, and it is typical to write proofs as tactic blocks.
We begin by outlining the most important kernel primitives related to universes, functions, and inductive types. We then take a brief look at tactics.