This chapter establishes the operational model of the Lean system.
This chapter establishes the operational model of the Lean system. The goal is to make the interaction between code, types, and proofs explicit at a small scale, so that later constructions behave predictably. Each component introduced here appears throughout the rest of the book, often in more complex forms, so the emphasis is on exact behavior rather than surface syntax.
Lean organizes work as a collection of modules compiled within a project managed by Lake. A project provides a dependency graph, a build plan, and a namespace boundary. Within this structure, every file contributes declarations to an environment. Understanding how names are resolved, how imports extend the environment, and how namespaces prevent collisions forms the basis for all larger developments.
The core language consists of expressions, definitions, and theorems. A definition introduces a term with a given type. A theorem introduces a term whose type is a proposition. There is no fundamental distinction at the kernel level between programs and proofs; both are terms checked by the same type system. This uniformity is the main source of power and the main source of confusion. The chapter isolates the minimal rules that govern this system: how functions are formed, how arguments are inferred, and how types are assigned.
A central mechanism is elaboration. The user writes partial expressions that omit arguments, types, or implicit structure. The elaborator reconstructs a complete term by inserting implicit arguments, resolving typeclass instances, and solving constraints. Many practical issues arise from this reconstruction process. The chapter introduces the tools that expose it: commands that display inferred types, commands that evaluate expressions, and techniques for controlling inference through explicit annotations.
Proof development is presented in two complementary styles. Term mode constructs proofs as explicit expressions. Tactic mode constructs proofs by transforming goals. Both styles produce the same underlying objects. The distinction is practical: term mode favors compactness and compositionality, while tactic mode favors stepwise construction and local reasoning. The chapter shows how to move between these styles and how to read the resulting terms.
Inductive types and structures appear early because they define the data that proofs manipulate. An inductive type specifies constructors and an associated recursion principle. A structure groups fields into a single object with named projections. These mechanisms support both computation and reasoning. The chapter focuses on their basic formation rules and on simple pattern matching, postponing more advanced recursion and dependent behavior.
The interactive workflow is treated as a first class component. Development proceeds by writing partial code, inspecting goals, refining expressions, and iterating. The editor integration exposes the current state of goals and the local context. Error messages are interpreted as constraints that failed to solve. The chapter provides a methodical approach to these interactions so that failures can be localized and corrected without guesswork.
By the end of the chapter, you will be able to construct small definitions, state and prove elementary theorems, and navigate the environment with confidence. More importantly, you will have a clear model of how Lean processes code: how a line of text becomes a fully elaborated term, how that term is checked, and how it is stored for later use. This model is used repeatedly in subsequent chapters to control automation, design interfaces, and scale proofs.