# Preface

This book is a working manual for the Lean proof assistant. It focuses on construction. Each section isolates a task, shows the minimal mechanism that solves it, and records the pattern in a form that you can reuse. The intent is operational fluency rather than exposition.

Lean treats propositions as types and proofs as programs. This correspondence makes it possible to write proofs with the same discipline used in programming: small interfaces, explicit data flow, and compositional design. The book adopts that viewpoint. Definitions are written to be consumed by later proofs. Lemmas are shaped to be rewritten by automation. Tactic scripts are organized so that failure modes are visible and local.

The material is arranged to reduce friction. Early chapters establish the core language, the proof model, and the tactic framework. Middle chapters develop the main tools: equality, inductive types, structures, typeclasses, and recursion. Later chapters address automation, metaprogramming, and the organization of large projects. The final chapters present complete developments that combine these pieces into end to end artifacts.

The style is intentionally compact. Each section contains a focused problem, a small set of definitions, and a proof or construction that exposes a general pattern. Explanations are direct and avoid digression. When a technique depends on library support, the dependency is made explicit. When a tactic is used, the reason for its success is stated in terms of the underlying rules.

A recurring theme is control of the elaborator and the simplifier. Many difficulties in Lean arise from implicit arguments, instance search, and rewriting that is too aggressive or too weak. The book shows how to make these mechanisms predictable: how to structure types so that inference succeeds, how to design simp lemmas so that normalization terminates, and how to localize automation to a goal.

Another theme is stability. Definitions and lemmas are written with an eye toward long term reuse. Names are chosen to reflect algebraic structure. Interfaces are kept minimal. Proofs prefer canonical forms so that later rewriting remains straightforward. These choices reduce the cost of refactoring and make large developments tractable.

The reader is expected to be comfortable with basic functional programming and elementary logic. No prior experience with Lean is assumed. The book can be read sequentially, but it also supports direct lookup. Section titles are action oriented, and examples are self contained.

This text does not attempt to duplicate the reference documentation of Lean or the library guides of mathlib. Instead, it provides a layer between reference material and large scale formalization. It records the small moves that make proofs go through, and it organizes them into a set of patterns that can be composed.

All code is intended to compile in a standard Lean project managed by Lake. Examples avoid unnecessary dependencies and highlight the minimal imports required. When performance or automation is relevant, alternative formulations are shown so that trade offs are visible.

Lean is a precise system. Small changes in types or hypotheses can change the shape of a proof. The approach here is to expose that precision and make it usable. After working through the patterns in this book, you should be able to design definitions that admit clean proofs, control automation when it matters, and scale a development without losing clarity.