Recommendation: The first Lean 4 milestone is a two-line proof with no errors, no sorry and a statement that matches its plain-language claim. Each declaration has three parts (parameters, goal and proof step), and reading those parts comes before learning more tactics.

Setup and the toolchain file

A beginner needs Lean installed and an editor that shows Lean's feedback next to the code. The official installation page is the reference for the current setup. Instructions copied from older articles can target a different toolchain, so the version that matters is the one the project pins.

A Lean project records that version in a lean-toolchain file at the repository root. Two commands check work from a terminal:

lake build
lake env lean Basic.lean

lake build: builds the whole project with the pinned toolchain and reports every error and warning.
lake env lean Basic.lean: checks one file. lake env sets up the project's dependency paths, so imports resolve the same way they do during lake build.

A learning log for each session records the repository revision, the file, the command and the first message Lean printed. When a later attempt fails, that record separates a change in the exercise from a change in the setup.

Three parts of a declaration

Lean treats propositions as types and proofs as terms of those types, as the official introduction to propositions and proofs explains. In practice, a declaration states a target type, and the proof supplies a term of that type.

Mind map of a Lean 4 example declaration split into parameters, goal and proof step

Every example in this post has the same three parts:

Parameters: everything in parentheses before the last colon. Lean shows them as the local context, the facts the proof may use.
Goal: the type after the last colon. Lean shows it after ⊢ in the infoview panel.
Proof step: the tactic block after := by. It must close the goal.

A first equality

example (sample : Nat) : sample = sample := by
  rfl

Reading the line part by part:

example: a declaration without a name. Lean checks it but nothing else can refer to it.
(sample : Nat): one parameter named sample of type Nat, the natural numbers.
: sample = sample: the goal, an equality.
:= by: starts a tactic proof.
rfl: closes goals of the form a = a, as described in the tactics chapter.

The claim covers every natural number, not a particular numeral. No calculation or test data is involved. Lean accepts the proof because both sides of the equality are the same term.

Using a hypothesis

The second example puts evidence in the context and asks for it back:

example (Claim : Prop) (evidence : Claim) : Claim := by
  exact evidence

(Claim : Prop) introduces a proposition. (evidence : Claim) introduces a proof of that proposition. The goal asks for Claim, and exact evidence supplies the term already in the context.

A three-column note keeps each step tied to the goal:

Part	Question	Example
Context	Which facts are available?	`evidence : Claim`
Goal	Which fact is required?	`Claim`
Step	Which term fits the goal?	`exact evidence`

The table is a reading aid, not Lean syntax. It turns a proof session into an account of why each step applies, instead of a search for commands that happen to work.

Reading error messages

Errors fall into two groups. Changing the goal of the second example to a different proposition makes exact evidence fail because the evidence no longer fits. That is a proof error. Renaming evidence in one place but not the other produces an unknown identifier. That is a text error. The fixes are different, so the first step is to tell them apart.

Lean separates errors from warnings, as the interaction chapter explains. A warning does not stop the file from checking, but it often points at something unfinished.

One useful exercise changes a single thing at a time: the parameter name in one session, the goal in the next, the proof step in a third. Comparing the messages builds the vocabulary needed to ask a precise question about a proof.

When a proof is finished

Mind map of three conditions for a finished Lean 4 proof: no errors, no placeholders and a statement that matches the prose claim

A finished proof meets all three conditions in the mind map.

No errors. lake build or the editor reports no errors for the file.

No placeholders. sorry lets Lean accept an unfinished proof with a warning. The tactic reference documents #print axioms, which lists the axioms a declaration depends on:

theorem self_eq (sample : Nat) : sample = sample := by
  sorry

#print axioms self_eq

theorem self_eq: a named declaration, so #print axioms can refer to it.
sorry: a placeholder. Lean prints the warning declaration uses 'sorry'.
#print axioms self_eq: reports 'self_eq' depends on axioms: [sorryAx]. Replacing sorry with rfl removes sorryAx from the list.

Statement matches. Lean checks that the proof proves the formal statement. It does not check that the formal statement says what the note says. Suppose a note claims that every measurement is positive, while the formal statement takes positivity as a hypothesis. A proof of that statement does not establish the note's claim. The record for each exercise therefore holds four things: the prose claim, the formal statement, its hypotheses and the finished proof.

A learning sequence after the first file

A suggested order, not a required curriculum:

Reflexive equalities with one explicit parameter.
Goals closed by a named hypothesis.
A statement with two hypotheses and a written note on which one the proof uses.
A library example with each imported lemma explained.
A small claim taken from an existing mathematical note.

Each stage ends when the proof can be explained step by step, not when a set number of exercises is done.

Frequently asked questions

Does a first proof need Mathlib?

No. Both examples above use only Lean's core library. Mathlib becomes useful for library mathematics, and the Mathematics in Lean basics chapter is a good next stage once goals and proof steps are familiar.

Can an AI assistant write the proof steps?

It can propose them. Lean then checks whether the step closes the goal. The explanation saved in the learning log should still be checked against the actual goal and the documentation, because an AI explanation can be wrong even when the step works.

What is the difference between `example` and `theorem`?

Both are checked the same way. theorem gives the result a name that later proofs and commands such as #print axioms can use. example has no name.

Oyren's maths notes feature pairs LaTeX notes with a separate Lean 4 and Mathlib Codespace. The note holds the prose claim and open questions, and the Codespace holds the formal proof. Oyren's Lean environment overview covers the setup.