4. From Nil to Nat: Arithmetic
Our next goal is to implement the natural numbers, arithmetic operations, and the machinery for proving theorems about them.
We'll create all of that out of little more than thin air.
Typically, specialized programming languages come chock-full of features relating to their niche: MatLab knows all about matrices right off the bat, the Excel spreadsheet suite suitably excels at spredsheets... In contrast, the Lean kernel, while designed to handle mathematical concepts, comes with zero of them built in.
There are no data types that represent numbers.
No int, no float, no bignum.
It has no concept of Boolean variables.
There are no algebraic operations.
Not even a relation "=" that would assert the equality of two objects.
All it offers natively are ways to define custom types and functions between them. (They didn't call it Lean for shits and giggles).
Now the library ecosystem around it comes with hundreds of megabytes of formalized mathematics. However, to get to know the system, we will forgo these ready-made results, and implement our own mini version of arithmetic from zero.
4.1. Warm-up: A finite type
4.1.1. Inductive types
To do anything at all, we need to define custom data types.
These are called inductive types in Lean, for reasons that will soon become clear.
One defines them using the inductive keyword
inductive metro : Type where
| rio : metro
| newyork : metro
| ehrenfeld : metro
This defines a type metro.
The names after the bars "|" are constructors for the type:
They represent all the ways in which an object of type metro can be created.
As there are three such ways in the example, metro is a data type that can take three different values.
The following statement creates an object of type metro with value rio and binds it to the name const
def const := metro.rio
Lean provides a few commands that start with a hashDear members of Generation Z. Yes, it is called a hash, not a "hash tag".
This ain't Twitter (or whatever people call their microblogging platform these days.)
"#" and are meant to be used interactively in the development phase.
Applied to our object
#reduce const -- bring a term into normal form
#check const -- show the type of a term
#print const -- show the definition of a term
Hover over the command to see its output.
You'll note the liberal use of colons :.
An expression of the form term : type are type judgments that express the fact that term has type type.
4.1.2. Functions
At this point, there's nothing we can do with the type, except instantiate it. So let's define a function.
open metro -- now we can write `rio` instead of `metro.rio`
def shuffle : metro -> metro := fun n => match n with
| rio => newyork
| newyork => ehrenfeld
| ehrenfeld => rio
#check shuffle -- `shuffle : metro → metro`
When we defined shuffle, we declared it to be of type metro -> metro.
In general, the arrow type α -> β
denotes the type of functions that take objects of type α and return objects of type β.
The expression "fun x => body" builds a function object.
When applied to an argument arg, all occurrences of x in the body will be replaced by arg.
The actual behavior of the function is defined using Lena's pattern matching facility,
which takes an argument and a list of of pairs | pattern => value.
If the argument matches a pattern, it is replaced by the corresponding value.
Unless indicated otherwise, Lean functions are total, i.e. must be well-defined for every possible input from the domain.
If the argument (like x here) is of an inductive type, this is assured if every constructor of the type matches one of the patterns provided.
Function application has the syntax function argument.
In math and in most programming languages, parentheses are overloaded.
They both group terms together and also separate a function name from its arguments.
Lean does use the former meaning, but not the latter
#reduce shuffle newyork -- `ehrenfeld`
In math and in most programming languages, parentheses are overloaded: They both group terms together and also separate a function name from its arguments. Lean does use the former meaning, but not the latter.
#reduce shuffle (shuffle rio) -- `ehrenfeld`
We can now handle finite data types, and functions whose behavior we have manually specified on all possible inputs. That's admittedly very boring. Things will get more spicy in the next section!
Remarks:
-
Did you notice the Greek
α, βabove? Lean goes all-in with Unicode. It accepts→for->and↦for=>. LaTeX syntax mostly works for input, like "\to" to get "→".
4.2. The natural numbers
Here's a much more exciting type declaration:
inductive nat : Type where
| zero : nat
| succ : nat → nat
The first constructor is a constant, nat.zero, as above.
The second constructor is a function that takes an argument of the type we're defining only now.
(Try that in your garden-variety programming language!)
To construct a first object of type nat, we must use zero, because succ requires us to provide a nat as an argument, and we've got to start somewhere.
open nat
def z := zero
But now that one exists, we can apply the second constructor to it
def one := succ z
and then repeat
def two := succ one
def three := succ two
#reduce three -- succ (succ (succ zero))
The possible objects of type nat are hence given exactly by n concatenations of succ applied to zero, for some number n.
In this sense, we have defined a legitimate model of the natural numbers!!
4.2.1. Functions on natural numbers
What about functions taking nat arguments?
We can no longer specify their value on all inputs explicitly.
But a function can handle any object of type nat as soon as we tell it how to handle those that have been created via the zero constructor and those that have been created by the succ constructor:
def predecessor : nat → nat := fun n => match n with
| zero => zero
| succ k => k
#reduce predecessor two
Just like type constructors, function definitions can be recursive
def double : nat → nat := fun
| zero => zero
| succ k => succ (succ (double k))
#reduce double two
All functions defined so far used the pattern matcher. Alternatively, one can combine existing functions
def plus_two : nat → nat := fun n => succ (succ n)
#reduce plus_two zero
Here's a function that takes two arguments (adding them)
def plus : nat → nat → nat := fun
| n, succ m => plus (succ n) m -- reduce rhs leaving
-- sum invariant; recurse
| n, zero => n
#reduce plus one two
(We're doing real math, here!)
The type of plus is nat → nat → nat, which associates as nat → (nat → nat).
Wait, what?
Under the hood, Lean functions only ever take one argument.
To model multi-argument functions, one uses a gadget called Currying:
Think of a function f: a × b → c as
f: a → (b → c), a ↦ (f(a, · ): b ↦ f(a, b))
That is, f takes the first argument and returns "itself with the first argument already plugged in".
Exercises.
-
Write a function
minusthat does what it says on the tin. Usezeroas a floor, as we don't have negative numbers yet.
-
Write a function
timesfor multiplication. You can re-useplus.
At this point, we've got the computational part of arithmetic in the bag. Below are a few more advanced topics for you to skim, then we'll go on to model logic.
4.3. Miscellaneous features
Here, we briefly mention more features of Lean's language that will be used in the following. This section might be expanded later -- for now, refer to the language reference for details.
4.3.1. Sweetening the deal
In computer language design, syntactic sugar refers to a construction that provides a simple ("sweet") user interface for a low-level feature, without adding any new functionality.
If cars were code, this would be syntactic sugar for the motor vehicle's directional control.
Any Lean code you write will go through a sequence of pre-processing steps (elaboration in Lean parlance) that rewrite the user-facing syntax into a more spartan form suitable for processing by the kernel.
Here are some sugary examples:
4.3.1.1. Parameters
Definitions can include named variables.
These are declared with the syntax (par : type) placed between the name of the object being defined and the colon that marks the beginning of the type information.
Lean then replaces the function body by "fun par => body", so that the parameters are accessible by name inside the body:
def plus_three (n : nat) : nat := succ (succ (succ n))
#reduce plus_three zero
4.3.1.2. Field notation
Instead of the function notation succ zero can use the more compact field notation zero.succ
#reduce zero.succ
#reduce zero.succ.succ
The general rules are explained in the language reference.
4.3.1.3. Implicit match
You can leave out the boilerplate "fun n => match n with":
def predecessor': nat → nat := fun
| zero => zero
| succ k => k
4.3.2. Higher-order functions
Arguments and return values can be of any type. This includes arrow types, i.e. functions
def do_twice (f : nat → nat) : nat → nat :=
fun n => f (f n)
def plus_four := do_twice plus_two
#check plus_four
#reduce plus_four zero
4.3.3. Apologize!
It is possible to declare that an object has a given type, without defining it. You have to apologize to the system, though
def unknown_nat : nat := sorry #check unknown_nat -- nat #reduce unknown_nat -- sorry
As we'll see later, this is how axioms are handled in the logics part.
4.4. Reduction
Let's peak behind the scenes a bit and see what #reduce actually does.
During reduction, the Lean kernel recursively applies a small number of rewriting rules to a term, until it no longer changes. These rules go back to the early days, when computer science was done by mathematicians -- and are thus labeled by Greek letters for maximal obscurity.
Let's start with the term
predecessor one
The two constants are replaced by their definitions -- a process pretentiously called δ reduction. Plugging in, we're left with
(fun n => match n with | zero => zero | succ k => k) (succ zero)
(As we'll see below, the match statement is also just sugar, and gets rewritten in terms of a recursor before being sent to the kernel. This doesn't effect the logic of this example, though).
The next step is function application or, uh, β reduction.
The bound variable n is replaced by the argument throughout the body
match (succ zero) with | zero => zero | succ k => k
Finally, case distinction is performed, under the name of ι reduction (more on the internals below), leaving us with zero, as intended.
(It's δ for definition, ι for inductive, and β... ...as far as I can tell because it was the second rewriting rule people wrote down, coming after α conversion, which refers to the renaming of bound variables. The letter "β" doesn't appear in Church's defining paper on the subject -- so I don't know whom to blame for this sorry state of nomenclature.)
There are two less-fundamental reduction rules (one for local definitions and one for quotient types). Together, these five simple rewriting rules essentially define how information processing is done in Lean's kernel.
4.4.1. Reduction vs evaluation
Lean's approach to formalized mathematics is based on the equivalence between proving and programming. However, in practice, a system optimized for mathematics would make very different trade-offs than a system optimized for producing general-purpose code. Lean chose... ...to do both!
We've seen above how to use the kernel's reduction rules to process information. But Lean also comes with a completely independent code generator, which can turn Lean programs into executable code. Since version 4, Lean itself is written largely in Lean!
You can run compiled versions of your own functions using the #eval command
#eval plus one two
#reduce plus one two
Confusingly, there are now two different ways to "compute things". However, the scope of these approaches is very different.
Reductions act symbolically on terms in the language.
(You can see that the #reduce command above produces Lean objects by inspecting its output in Visual Studio Code's InfoView).
Any term can be reduced, including terms that describe types, undefined constants (i.e. sorry), or proofs (to be introduced next)
#reduce nat -- nat #reduce unknown_nat -- sorry
#eval only handles the "computational fragment" of Lean.
As of 2025, I don't think the language reference includes a concise definition of what precisely this entails -- but the fragment certainly excludes types, proofs, and undefined constants.
That's compatible with the approach of conventional compiled languages, which use type information only for code generation and static analysis:
There's no way to recover the typing choices of the programmer knowing only the output of a program written in C.
Consequently the following commands wil all fail
#eval nat -- cannot evaluate, types are not computationally relevant #eval unknown_nat -- aborting evaluation since the expression depends on the 'sorry' axiom [...] #eval! unknown_nat -- cannot evaluate code because 'unknown_nat' uses 'sorry'
Also, if you inspect the output of #eval one two in VSC, you'll find that the the code produced a string, not a Lean object.
There's another difference: As discussed next, Lean will make sure that the reduction process never enters an infinite loop.
While desirable for math, it would be too burdensome to ask programmers to supply a termination proof for every loop they write.
This guardrail is therefore not present in #eval.
As a consequence, #eval runs much faster than #reduce and can handle much more complex calculations before exhausting your computer's resources.
4.5. Three hails for the recursor
Lean's match statement for defining functions from inductive types is syntactic sugar.
Before your program gets passed to the kernel, match code blocks are re-written in terms of an object that's fundamental to Lean's logic: the type's recursor.
The recursor is a function symbol created by Lean whenever an inductive type is declared. It is "dual" to the constructors in the sense that the constructors list all the ways an object of the given type can be created, while the recursor specifies exactly how such objects can be eliminated.
Neither the constructors nor the recursor can be defined in terms of more primitive Lean functions using def.
The kernel will thus not unfold them using δ-reduction.
Instead, recursors are exactly the objects that get handled by the ι-reduction rules.
Concretely, consider a type α with constructors con₁, ..., conₙ.
The type's recursor takes parameters elim₁, ..., elimₙ.
Then F := α.rec elim₁ ... elimₙ is a function on α.
The argument elimᵢ determines how F will act on objects that have been constructed with conᵢ.
The details are particularly easy for finite types, i.e. types where the constructors take no arguments.
In this case, each elimᵢ is just a constant, and F conᵢ reduces to elimᵢ.
For example:
noncomputable def shuffle_rec : metro → metro :=
metro.rec newyork ehrenfeld rio
#reduce shuffle_rec rio -- newyork
(The weird noncomputable keyword is explained below, don't worry for now).
In fact, our previous definition in terms of match got internally rewritten into exactly this form:
#reduce shuffle
#reduce shuffle_rec
Now say we want to define a function F : nat → nat.
The first constructor nat.zero is just a constant, and so elim₁ is a constant as well.
But con₂ is nat.succ: nat → nat, which is clearly more interesting.
To tell the recursor how to handle F (succ k), one specifies a function elim₂ that has two arguments.
Then ι-reduction will rewrite F (succ k) as elim₂ k (F k).
Note that the second argument results from a recursion, hence the name.
Here's a re-implementation of the predecessor function in terms of nat.rec
noncomputable def pred_rec : nat → nat :=
nat.rec zero (fun k r => k)
#reduce pred_rec one
Computing the predecessor doesn't involve recursion, so the second argument goes unused.
In contrast, double does use recursion
noncomputable def double_rec : nat → nat :=
nat.rec zero (fun k r => r.succ.succ)
#reduce double_rec two
Unlike the original double function, elim₂ no longer refers to itself
(manifestly so: it is an anonymous function that is not assigned a name that could be referenced).
The recursion is realized by ι-reduction supplying the result of F k as one of the arguments to elim₂.
It is also clear that this recursion will terminate:
In order to find F (succ k), the kernel only needs to know F k, i.e. the function evaluated on the argument with one constructor removed ("recursion by removing a constructor" is called structural recursion in Lean).
But all objects of an inductive type arise from the action of finitely many constructors on constant constructors (like nat.zero).
As part of the elaboration process, Lean code destined for the kernel will undergo a recursion elimination process, where self-referential functions are rewritten in terms of recursors. By the above argument, this guarantees that the reduction process will not get stuck in an infinite loop.
4.5.1. Remark on computability
The computational part of Lean does support potentially non-terminating recursions.
Recursion elimination is thus not performed on code destined for the compiler (see this diagram).
In fact, Lean 4 as of revision 25 does not even support compiling functions directly defined in terms of recursors.
While there seem to be good pragmatic reasons for delaying its implementation, it is in my opinion somewhat unfortunate that a feature that is fundamental to Lean's logic is not reflected in the computational fragment.
This current limitation is the reason for the noncomputable attributes seen above.
4.5.2. The church of the recursor
Finally, let's get a bit philosophical.
The (somewhat complicated) type of nat.rec says that if you supply it with elim₁ and elim₂, it will give you a total function on nat.
You can read this as a promise, or if you wish, an axiom.
Of course, the developers didn't just make up this claim!
They wrote code implementing ι-reduction, which will compute the function on any input...
...or at least any input that the physical computer Lean is running on can handle.
Now recall our brief discussion of the Aristotelian realist philosophy of mathematics. If the soundness of math is backed up by the properties of physical objects, then one could content that computations that surpass the capabilities of any realizable computer are not a meaningful concept. My favorite fringe group of metamathematicians, the ultrafinitists, are ready to bite that bullet. They would reject the promise implied by the recursor's type. In contrast, mainstream math accepts that this mild generalization of what the computational backend actually delivers on will not lead to conceptual difficulties.
I'm going on and on about this, because as we will soon see, all Peano axioms, including the axiom scheme of induction, become theorems once you accept the recursor's type.
Thus, believing in Lean's logic essentially boils down to confessing your faith in this particular type judgement.
Hence this section title. (Hooray! Hooray! Hooray!)