6.1.1. Types and terms🔗

The first thing to get used to is that Lean does not speak the language of set theory directly. Mathematicians usually say that ℝ is a set and that 37 ∈ ℝ. Lean uses type theory instead. In Lean, ℝ is a type and 37 is a term of that type. The notation (37 : ℝ) should be read as "37 has type ℝ" (the parentheses only group the expression here). This is the Lean analogue of saying that 37 is an element of the real numbers.

In Lean, every expression has a type. If E is the space, then (E : Type) says that E is a type, and (x : E) says that x is a term of that type. In mathematical language, we would say that E is our space and that x is an element of it.

6.1.2. Universes🔗

Remember: in Lean, every expression has a type. Therefore, types themselves must also have a type. The universe in which ordinary mathematical types live is called Type. For example, (ℝ : Type) says that the real numbers form a type, and (E : Type) says the same about our abstract space.

This gives a three-level mental picture:

Type        universe
ℝ, E, ℕ     types
37, x, n    terms

This picture is not the full story, because Lean has a hierarchy of universes (Type 0, Type 1, and so on) to avoid the usual paradoxes around "the collection of all collections". For the purpose of reading most of the code we will write, it is usually enough to remember that objects such as groups, rings, and vector spaces live as types, while their elements live as terms.

6.1.3. Function types🔗

If X and Y are types, then X → Y is the type of functions from X to Y. Thus (f : X → Y) means that f is a term whose type is X → Y; in usual mathematical language, f is a function from X to Y.

To apply a function to an argument, Lean simply writes the function and then the argument, separated by a space. So if (a : X), then (f a : Y) is the value of f at a. In ordinary mathematical notation we might write this as f(a), but in Lean the parentheses are usually only written when necessary to remove ambiguity.

For example, if E is a type representing a Banach lattice, a sequence in E can be represented by a function (u : Nat → E), because it takes a natural number and returns an element of E. The term (u 0 : E) is the first value of the sequence, and (u 3 : E) is another value.

6.1.4. Propositions and proofs🔗

Lean also has to talk about theorem statements and proofs. Here the same type-and-term idea appears again: propositions live in a universe called Prop.

For instance, the statements 2 + 2 = 4 and 2 + 2 = 5 are both propositions. In Lean notation, they have type Prop: (2 + 2 = 4 : Prop) and (2 + 2 = 5 : Prop).

The surprising part is that proofs are also terms. That is, in type theory proofs are part of the theory itself. If we have (rfl : 2 + 2 = 4), then this term has type the proposition 2 + 2 = 4. This is what in ordinary mathematical language we interpret as a proof of that statement. On the other hand, I can assure you that it is impossible to construct (under the usual axioms) a term of type 2 + 2 = 5, because that would constitute a proof of the proposition 2 + 2 = 5.

So the same notation x : X covers two situations that mathematicians usually separate:

x : E        x is an element of the space (E : Type)
h : P        h is a proof of the proposition (P : Prop)

This takes a little time to sink in and feel natural.

6.1.5. Implication as a function🔗

The notation for functions and the notation for implication are the same in Lean: P → Q. This is not an accident. If P and Q are ordinary types, then P → Q is the type of functions from P to Q. If P and Q are propositions, then P → Q is the proposition "if P, then Q".

This may seem weird at first, but the more you think about it, the more sense it makes. A proof of P → Q is something that takes a proof of P and returns a proof of Q. So when the context contains (h : P → Q) and (hp : P), you should read h hp as the proof of Q obtained by applying the implication h to the proof hp.

6.2.1. Structures🔗

A structure is a type with named fields. For instance, a very small structure could package a type together with a distinguished point:

A term of type PointedType is therefore a pair: first a type, and then a term of that type. The important point is not this particular example, but the pattern. Structures are how Lean turns "an object with some extra data" into an actual type.

Here is a more mathematical example. A group structure on a type G can also be described as:

This is not the definition of groups in mathlib, but it shows the idea. A term of type MyGroupStructure G is a package containing three pieces of data, namely multiplication, the identity element, and an inverse map, together with proofs of the group axioms. If s : MyGroupStructure G, then the multiplication is s.mul, the identity is s.one, and the inverse function is s.inv.

The Equiv structure is another mathematical example. If X and Y are types, then X ≃ Y is the type of equivalences between them (≃ is just notation for Equiv). A term (eXY : X ≃ Y) contains four fields:

toFun     : X → Y
invFun    : Y → X
left_inv  : LeftInverse invFun toFun
right_inv : RightInverse invFun toFun

The first two fields are the two functions. The last two fields are proofs saying that the functions are inverse to each other. Thus an equivalence is not merely a function which happens to be bijective in our head; in Lean it is a function, an inverse function, and the proofs that they compose correctly.

Once a structure has been defined, Lean automatically gives us projections for its fields. If (eXY : X ≃ Y), then (eXY.toFun : X → Y) is the forward function and (eXY.invFun : Y → X) is the inverse function. This notation is called dot notation. It means: take the object before the dot and extract the named field after the dot.

There is one more thing going on here. Lean lets us write (eXY a : Y) instead of eXY.toFun a. In other words, Lean can treat an equivalence as its underlying function when the context asks for a function. This is called a coercion. We will talk more about coercions later.

6.2.2. Classes🔗

The structure MyGroupStructure above is an honest way to package the definition of a group, but it would be inconvenient to use directly. If s : MyGroupStructure G and a b : G, then the product of a and b would be s.mul a b. The inverse of a would be s.inv a. Every lemma about groups would also have to mention the "group structure" s explicitly. That is not how mathematicians speak. Once we say "let G be a group", the group structure is always implicit, and rarely cited explicitly.

This is what classes are for. A class is a structure which Lean is allowed to search for automatically. A version of the previous group structure, now written as a class, looks like this:

This is deliberately the same structure as before: multiplication, an identity element, inverse, and proofs of the axioms. The difference is how Lean is allowed to use the structure. A term of type MyGroupStructure G is an ordinary argument. A term of type MyGroupClass G is an instance, so Lean can try to find it automatically using a procedure called "type class instance inference".

A declaration such as

should be read as:

Let G be a type, and assume that Lean can find a group structure on G.

If a later definition or theorem asks for a MyGroupClass G structure, Lean will look through the available instances and try to fill it in silently. If it cannot find one, the usual error says that Lean failed to synthesize an instance.

The keyword instance is how we make Lean aware that a type has a certain structure. Here is a tiny example, much simpler than groups:

The class MyChosenPoint X means: a type X together with a chosen point of X. The declaration starting with instance tells Lean that Nat has the structure of a "type with a chosen point", and in particular we set this chosen point to be 0. After that, whenever Lean needs a term of type MyChosenPoint Nat, it can find this declaration by itself. The term inferInstance is a way of explicitly asking Lean to perform that search.

In ordinary mathematics, this is close to saying "from now on, use this structure on this object unless told otherwise". For example, mathlib contains instances telling Lean that ℝ is a group under addition, a field, an ordered field, a topological space, and many other things. Most of the time we do not name those instances directly.

A group homomorphism could be defined like this:

The term MyGroupHom G H means: a function from G to H, together with a proof that it preserves multiplication. This is an ordinary structure, because we may want to talk about several different homomorphisms between the same two groups.

It is not uncommon in Lean for a theorem to start with a long list of assumptions such as [Group G], [TopologicalSpace X], or [Module ℝ E]. These are not extra variables that the proof is going to manipulate directly. They are instructions to Lean's typeclass system: keep these structures available, and use them whenever the notation and lemmas require them. If [Module ℝ E] is in the context, and you have a : ℝ and x : E, then a • x : E will make sense to Lean (where • is Lean's standard notation for scalar multiplication).

6.2.3. Extending structures and classes🔗

The group examples above repeat a lot of information. A group is a monoid with inverses. If we have already packaged the monoid part, we should not have to write it again from scratch.

Lean has an extends syntax for this. First we can package the monoid data and axioms:

Then a group structure can extend this monoid structure by adding only the inverse operation and the inverse axioms:

This means that a term of type MyGroupStructure₂ G has all the fields of MyMonoidStructure G, plus the new fields written in the second structure. If s : MyGroupStructure₂ G, then s.mul, s.one, and s.inv are all available.

The same idea applies to classes. We can first define a monoid class:

and then extend it to a group class:

Now a [MyGroupClass₂ G] instance also provides a [MyMonoidClass G] instance. This is extremely useful in large libraries. A theorem about monoids should work for every group, because every group is in particular a monoid. The extension mechanism is how Lean organizes this hierarchy without duplicating the same fields and assumptions over and over.

6.3.1. Round brackets🔗

Consider the associative law for groups:

Inputs in round brackets are explicit inputs. If a theorem has (a b c : G), then these are the pieces of data that we normally write when applying the theorem.

For example, in our current context we have a group G and elements g1, g2. The term (mul_assoc g1 g2 g1 : g1 * g2 * g1 = g1 * (g2 * g1)) is the associativity theorem applied to the three explicit inputs g1, g2, and g1. Notice that we did not write the type G or the semigroup structure on G. Those are not round-bracket inputs in the displayed type of mul_assoc.

6.3.2. Curly brackets🔗

Inputs in curly brackets are implicit inputs. They are real inputs to the function, but Lean tries to reconstruct them automagically from the inputs that we do write.

Consider the commutativity of addition:

Here {G : Type u} is not something we usually supply. If we write add_comm (1 : ℝ) (2 : ℝ), Lean sees that the first explicit input has type ℝ, so the hidden type G must be ℝ. This kind of reconstruction is done by Lean's unifier.

Another typical pattern is that a proof reveals the objects it is about. For instance:

The inputs α, β, a₁, and a₂ are implicit. If we give Lean a function f and a proof h : a₁ = a₂, the types of these explicit arguments contain enough information for Lean to infer the hidden ones.

So {x : X} should be read as:

Lean needs some `x` of type `X`, but expects to infer it from the surrounding
expression.

There is also a stricter form of implicit brackets, written ⦃x : X⦄. For reading code, you can almost always think of these in the same way as ordinary curly brackets: they are hidden inputs. The difference is about when Lean starts trying to infer them.

6.3.3. Square brackets🔗

As already explained, inputs in square brackets are also implicit, but they are inferred by a different mechanism: typeclass inference.

6.3.4. Overriding hidden inputs🔗

Sometimes Lean cannot infer an implicit input, or we want to force a particular choice. Then we can give the hidden input by name.

For example:

The expression (G := ℝ) tells Lean to use ℝ for the implicit input called G. This syntax is very useful when Lean has several possible ways to read an expression, or when an error message shows that an implicit argument was not guessed in the way we intended.

There is also a more forceful notation: putting @ before a theorem or definition exposes its hidden inputs.

The _ is a placeholder: it says "Lean, please infer this one". In the last example, the first _ asks Lean to infer the type, and the second one asks Lean to infer the semigroup structure. Thus @ lets us expose the hidden arguments, while _ lets us hand some of them back to Lean.

As a rule of thumb, when reading a Lean theorem statement:

(x : X)    explicit input; expect to see it when the theorem is applied
{x : X}    implicit input; Lean tries to infer it by unification
⦃x : X⦄   strict implicit input; also implicit, with slightly different timing
[C X]      typeclass input; Lean searches for an instance

All four kinds of inputs are part of the theorem. The brackets only tell us who is responsible for supplying them: the person writing the term, Lean's unifier, or Lean's typeclass system.

6.4.1. Coercions to functions🔗

Coercions are not only used between number systems. They are also used to treat structured objects as some simpler object inside them.

We have already seen this with equivalences. If (eXY : X ≃ Y), then eXY is not just a function. It is a structure containing a function from X to Y, an inverse function from Y to X, and proofs that these functions are inverse to each other. Even so, Lean lets us write (eXY a : Y) whenever (a : X). Lean has thus been instructed to silently use the forward function stored inside the equivalence.

The same thing happens with homomorphisms:

Here φ is a group homomorphism from G to H. As seen before, φ is a structure containing both a function and a proof that the function respects multiplication. When we write φ g, Lean coerces the homomorphism to its underlying function. The symbol ⇑ is the version of the coercion symbol used when a term is being treated as a function.

6.4.2. Coercions to types🔗

There is one more common coercion which is very important in mathematics: Lean can sometimes coerce a term to a type.

A subset of the real numbers is a term of type Set ℝ. It is not itself a type. Nevertheless, Lean lets us write a : s when s : Set ℝ. What this really means is that a is a term of the subtype of real numbers belonging to s.

If s : Set ℝ, then the type s is displayed by Lean as ↑s. A term a : s contains two pieces of information: a real number, and a proof that this real number belongs to s. The expression (a : ℝ) extracts the underlying real number. The proof that it belongs to s is a.property.

This is the same mathematical habit as saying "let a ∈ s" and then using a both as an element of the subset and as a real number. Lean keeps the two meanings formally separate, and coercions are the device which lets us move between them without writing all the bookkeeping by hand.

6.5.1. Basic tactics🔗

The tactic rfl proves equalities which are true by computation or definition.

The tactic intro introduces assumptions from an implication. In the next example, the statement says "if P and then Q, then P". The two calls to intro move the assumptions into the local context.

The tactic apply uses a theorem or hypothesis backwards. If the goal is Q and we apply a proof of P → Q, Lean changes the goal to P.

The tactic constructor splits a goal whose proof is made from several pieces. For a conjunction, it creates two goals.

The tactic rw rewrites using an equality.

Finally, simp is Lean's simplifier. It uses a large collection of standard simplification lemmas. For example, it knows that adding zero on the right does nothing.

This is only the very beginning. In real proofs you will also see tactics such as have, specialize, cases, induction, change, refine, linarith, ring, norm_num, aesop, and many others.

The term sorry is a placeholder for a missing proof. It can appear where Lean expects a term, and in particular where Lean expects a proof:

example : 2 + 2 = 4 := by
  sorry

Lean will accept this, but it produces a warning. Mathematically, a theorem proved with sorry has not been proved. Lean is being told to trust the missing proof temporarily.

This is useful when scaffolding a file. We can first write definitions and theorem statements, fill proof bodies with sorry, and check that the statements themselves make sense. Later, the sorrys must be replaced by real proofs. A Lean proof cannot contain any sorrys.

6.6.1. Is the code in a Lean project?🔗

A single Lean file sitting somewhere on your computer is not enough. Lean and mathlib change over time. A file may compile today on your machine and fail tomorrow, or fail immediately on someone else's machine, because a different version of Lean or mathlib is being used.

A Lean project fixes this problem. Files such as lakefile.toml, lake-manifest.json, and lean-toolchain record how the project is built and which versions of the dependencies are being used. This is why we work inside a repository, rather than sending isolated .lean files around. The repository is the reproducible mathematical environment.

6.6.2. Does the project build?🔗

The next check is mechanical. From the root of the project, run:

lake build

If this command finishes without errors, Lean has successfully checked the files which belong to the build. If it fails, then the project has not been verified in its current state. (Usually Codex will run this for you using its MCP.)

However, there is a subtle point. A file can exist in the repository without being imported by the project. In that case, lake build may succeed while the file containing your alleged proof is not being checked at all. In a typical project, the root file imports the files which should be built. For example, to make sure Convergences/Order.lean is compiled (this is the file we will add to the library in the next chapter), the root file BanLat.lean must contain:

import BanLat.Convergences.Order

Otherwise the proof is just text in the repository; it is not part of the verified build.

6.6.3. Are there placeholders or new axioms?🔗

At this point it is useful to separate three different questions which are easy to confuse:

Does the file compile?
Does the theorem have a real proof, rather than a placeholder?
Does the formal statement say what I meant informally?

Lean can answer the first two very well. The third one is still a human responsibility.

When Lean accepts a theorem, it has checked a proof term whose type is exactly the theorem statement. Tactics do not bypass this. A tactic such as simp, rw, or linarith is only a program which helps build the proof term; the small trusted kernel of Lean then checks the final term. This is why it is fine that proofs written by an LLM are often hard to read on a first pass: the LLM is not being trusted as a mathematician. Lean is checking the result.

For example:

The command #print axioms checked_two_add_two asks Lean which axioms the theorem depends on. For this tiny theorem, Lean reports that there are none.

This matters because a file can compile for the wrong reason. We have already seen sorry, which is a temporary hole in a proof. There is an even more direct way to make Lean assume something: one can declare an axiom.

axiom fake_proof : 2 + 2 = 5

theorem bad_example : 2 + 2 = 5 := fake_proof

This would compile, but it would not be a proof that 2 + 2 = 5. It would merely tell Lean to accept fake_proof as a new primitive assumption. If we printed the axioms of bad_example, we would see that it depends on fake_proof.

So, when checking code produced by Codex, there are two mechanical checks to keep in mind. First, the file should compile without warnings about sorry. Second, theorems should not depend on new axioms introduced by the file. The command #print axioms theorem_name is the basic diagnostic for the second point.

If #print axioms theorem_name mentions sorryAx, then some proof was omitted. If it mentions an axiom introduced in your project, then your theorem depends on an extra assumption which has not itself been proved. Both cases mean that the theorem is not yet proved in the ordinary sense.

6.6.4. Did you prove the theorem you claim?🔗

The remaining question is subtler. Lean proves exactly the statement you wrote, not the statement you had in mind. If the formal theorem is too weak, has the wrong hypotheses, uses the wrong notion of convergence, or talks about a different object after a coercion, then a perfect Lean proof will not fix the mathematical mismatch. This is why the state mode/prove mode split in our workflow is important. First we inspect the definitions and theorem statements carefully. Only after that do we ask Codex to fill the proofs.

There are several ways to fool yourself here. You can give a theorem a grand name, but the name is not checked by Lean. A declaration called RiemannHypothesis is only a proof of the Riemann hypothesis if its type is actually a faithful formal statement of the Riemann hypothesis. You can also define a statement and confuse this with proving it. Finally, Lean's notation is flexible: local notation, local definitions, and typeclass instances can make expressions look familiar while meaning something different from the standard mathematical object.

This is the part which cannot be delegated entirely to the kernel or the LLM. Lean checks that the proof proves the formal statement. Mathematicians must check that the formal statement is the intended one.

Thus the practical meaning of "we have proved it" is:

1. The result is in a reproducible Lean project.

2. The project builds with lake build.

3. The file containing the result is actually part of the build.

4. There are no sorries in the relevant declarations.

5. The theorem does not depend on unintended new axioms.

6. The formal statement has been checked against the informal theorem.

Once these checks pass, the proof does not depend on trusting Codex, or on trusting that a long tactic script "looks right". It depends on the Lean kernel checking a precise formal object.