brain

Backward reasoning starts from the goal and reduces it to simpler subgoals.

Rewriting with equality is one of the most frequent operations in Lean.

Forward reasoning starts from the assumptions in the local context and derives new facts until the goal becomes immediate.

An assumption is a local term that Lean may use to solve the current goal or produce another proof.

The local context is the list of variables, hypotheses, instances, and intermediate facts available at a point in a proof.

A Lean proof should expose the shape of the argument.

Every logical connective in Lean has two sides.

Names in Lean carry meaning.

Case analysis is the proof pattern for using data that has more than one possible constructor.

Proof by contradiction is a classical proof pattern.

A universal statement asserts that a property holds for every element of a type.

Lean is constructive by default.

Equality supports two structural operations: reversing direction (symmetry) and chaining steps (transitivity).

An existential statement says that some object exists with a given property.

Rewriting is the main way to use equality in Lean.

`False` is the proposition with no constructors.

Negation represents "not".

`True` is the proposition that always has a proof.

Equality expresses that two terms are identical.

Conjunction represents "and".

Lean identifies propositions with types and proofs with terms.

Implication is the first logical connective to understand in Lean because it is also the ordinary function type.

Disjunction represents "or".

Lean is normally developed inside an editor with live feedback.

Lean development is interactive.

A minimal working example is the smallest complete Lean fragment that demonstrates a definition, theorem, error, or technique.

Imports control what a Lean file can see.

Lean’s error messages report failed constraints during elaboration.

Lean development is driven by goals.

Lean proofs are terms.

A structure is a type whose values are built from named fields.

Tactic mode is an interactive way to build proofs.

Inductive types define data by listing its constructors.

Lean can execute many expressions during development.

Type checking is the primary feedback mechanism in Lean.

Pattern matching defines functions by cases on the shape of their inputs.

Lean files serve two readers at once: the compiler and the human maintainer.

Rewriting replaces one expression with another using an equality.

A definition introduces a named term together with its type.

Functions are the main form of computation in Lean.

Lean development is organized around projects.

Lean is a dependently typed system.

Lean functions often contain arguments that the user does not write.

Lean code is built from expressions.

Lean treats a theorem as a named proof.

Lean notation is ordinary syntax attached to ordinary declarations.

Lean organizes code as a hierarchy of modules.

This book is a working manual for the Lean proof assistant.

Lean is distributed as a small toolchain rather than as a single editor plugin.

Grammars, syntax, automata theory, regular and context free languages, parsing, recognition, and applications in compilers.

Simple type theory, dependent types, Curry-Howard correspondence, proof assistants, and formalized mathematics.

Simple type theory, dependent types, Curry-Howard correspondence, proof assistants, and formalized mathematics.

Logic programming, type systems, verification, model checking, and program synthesis.

Logicism, formalism, intuitionism, structuralism, and modern perspectives on the foundations of mathematics.

Logicism, formalism, intuitionism, structuralism, and modern perspectives on the foundations of mathematics.

Incompleteness, undecidability, independence, practical implications, and future directions in logic and foundations.

Proof theoretic ordinals, transfinite induction, strength of theories, applications to arithmetic, and limits of formal strength.

Constructive semantics, proof interpretation, differences from classical logic, Kripke models, and applications in computation.

Logic programming, type systems, verification, model checking, and program synthesis.

Consequences of incompleteness for truth, provability, independence, and the structure of formal systems.

Stronger forms of incompleteness, Rosser’s improvement, Löb’s theorem, and connections to computability.

Encoding symbols, formulas, and proofs as natural numbers to allow arithmetic to reason about its own syntax.

Proof that no sufficiently strong consistent system can prove its own consistency.

Arithmetization of syntax, the first and second incompleteness theorems, implications for formal systems, and refinements.

Construction of a true but unprovable statement using diagonalization and self-reference.

Quantitative study of proofs, including proof size, efficiency, and connections to computational complexity.

Formal structure of proofs, including derivations, inference rules, axioms, and proof representations.

Normalization of proofs, elimination of detours, and structural simplification of derivations.

Syntax of proofs, derivability, normal forms, consistency proofs, proof length, and proof complexity.

Methods for proving consistency of formal systems, including syntactic and semantic approaches.

Formal notion of deriving formulas from assumptions, including structural properties and inference behavior.

Sets that can be enumerated by algorithms and their role in semi-decidability and computability theory.

Existence of intermediate degrees between computable sets and the halting problem.

Global properties of the Turing degrees including incomparability, density, and jump structure.

Formal methods for comparing decision problems using many-one and Turing reducibility.

Equivalence classes of sets under Turing reducibility and the ordering of computational power.

Reducibility, Turing degrees, recursively enumerable sets, Post's problem, and the structure of degrees.

The undecidable problem of determining whether a Turing machine halts on a given input.

Extensions of undecidability using reductions and general results such as Rice’s theorem.

Step-by-step evolution of Turing machine configurations and how computations are represented as traces.

Machines that simulate any other Turing machine, establishing the concept of programmable computation.

Formal definition of Turing machines, including states, tape, alphabets, and transition functions.

Turing machine definitions, computation traces, universal machines, the halting problem, and undecidability results.

Detailed equivalence proofs between Turing machines, recursive functions, and lambda calculus, with explicit constructions and simulations.

Turing machines, register machines, lambda calculus, recursive functions, and the precise mathematical models used to define computation.

The Church Turing thesis, formal models of computation, equivalence of models, and the distinction between mathematical theorem and foundational principle.

Distinction between partial and total computable functions, undefined values, domains of definition, and the role of nontermination.

Primitive recursive functions, general recursive functions, minimization, and the formal construction of computable numerical functions.

Recursive functions, partial and total functions, the Church-Turing thesis, formal models of computation, and equivalence of models.

An introduction to infinite games, determined games, the axiom of determinacy, projective determinacy, and consequences for sets of reals.

Applications of advanced set theory to analysis and topology, including regularity properties, Banach spaces, measure theory, and topological classification.

An introduction to Polish spaces, Borel sets, analytic sets, projective sets, regularity properties, and the role of definability in set theory.

Forcing, large cardinals, descriptive set theory, determinacy principles, and applications in analysis and topology.

An introduction to large cardinal axioms, inaccessible cardinals, measurable cardinals, elementary embeddings, and consistency strength.

An introduction to forcing, generic filters, forcing names, the forcing relation, and the basic extension theorem.

The axiom of choice, choice functions, indexed families, and first consequences in axiomatic set theory.

The constructible universe, definable subsets, the hierarchy L_alpha, and the axiom of constructibility.

Equivalent forms of the axiom of choice, including Zorn's lemma, the well ordering theorem, maximal principles, and right inverses of surjections.

Independence results in set theory, including the axiom of choice and the continuum hypothesis, and the methods used to establish independence.

Relative consistency, inner models, constructibility, and the role of consistency results in axiomatic set theory.