Contents

Introduction<br>Less ThanPrograms And Proofs<br>Inductive Types<br>Functions<br>Less Than Revisited<br>Zero Is Less Than Successors<br>Addition And Transitivity

Insertion SortLists<br>Lower Bound<br>Sorted<br>Total Order<br>Algorithm<br>Sorted Output

-->

Formal Verification With Lean

30 Apr 2026

Introduction

Lean is a functional<br>programming language whose type system is powerful enough to encode mathematical propositions and proofs.<br>An important implication is that it is possible to use lean both to write programs and to<br>verify mathematical proofs about their properties.

The goal of this post is to introduce lean, use it to implement insertion sort<br>and prove that the output of our implementation is always sorted.

As a warm up, we’ll define the LessThan relation on natural numbers and prove basic<br>properties such as transitivity.

Next we’ll define the IsLowerBound and IsSorted list properties which are needed<br>to state and prove the correctness of insertion sort.

Finally, we’ll implement insertion sort and prove that its output is always sorted.

Note that a full correctness proof of would include a proof that the output of<br>insertion sort is a permutation of the input. This permutation property was<br>omitted in the interest of space and can be proved using similar techniques<br>to the ones in this post.

Less Than

Lean bridges the gap between programs and proofs via<br>dependent types.

To see how this works, we’ll use dependent types to define a LessThan relation<br>on natural numbers and prove some of its properties.

Programs And Proofs

In this section we’ll introduce the LessThan type and give a high level<br>overview of the relationship between programs and proofs.

The specifics of the lean syntax will be provided in the following sections.

The LessThan type represents the “less than” relation between pairs of natural numbers.<br>It is defined as follows:

inductive LessThan (n : Nat) : Nat → Prop where<br>| base : LessThan n (n + 1)<br>| step : {m : Nat} → LessThan n m → LessThan n (m + 1)

At a high level, this means that LessThan defines a family of types.<br>For each pair of natural numbers n m : Nat there is a corresponding type LessThan n m.<br>Instances of types in the family can be built inductively via the base and step constructors.

For example, we can use the base constructor to build objects of type<br>LessThan n (n + 1) for some n : Nat:

(.base : LessThan 3 4)

We can then use the step constructor to increment the m index:

(.step .base : LessThan 3 5)

By recursively calling .step we can construct objects in LessThan n m for all<br>n m : Nat satisfying n . For example:

(.step (.step .base) : LessThan 3 6)

We call LessThan a dependent type because each pair of natural numbers n m : Nat<br>defines a different type LessThan n m.

The Prop in the definition means that types in this family (such as LessThan 3 4)<br>belong to special class of types called propositions. In lean a proposition type is<br>defined to be true if an instance of that type exists and false if not.<br>An instance of a Prop type is called a proof of the proposition.

For example, LessThan 3 4 is a proposition and we can write this explicitly as

LessThan 3 4 : Prop

Furthermore, this proposition is true and the proof is the object we constructed above<br>with the base constructor:

(.base : LessThan 3 4)

We can declare the relationship between the proposition and the proof more explicitly<br>using the theorem keyword:

theorem three_lt_four : LessThan 3 4 := .base

As an example of a false proposition, consider

LessThan 0 0 : Prop

Indeed, it is easy to see that neither of<br>the two constructors of LessThan can output an object of type LessThan 0 0.<br>For example the LessThan.base constructor always outputs objects of type LessThan n n + 1<br>for some natural number n : Nat. We can verify this using lean via:

theorem not_zero_lt_zero : LessThan 0 0 → False<br>| h => nomatch h

Here the nomatch keyword asserts that there are no constructors matching<br>LessThan 0 0. We’ll discuss lean’s matching syntax in detail below.

Inductive Types

A common pattern in lean is to define objects inductively. Indeed, the natural<br>number type Nat is an inductive type with two constructors:

inductive Nat where<br>| zero : Nat<br>| succ (n : Nat) : Nat

This type has two constructors:

zero : Constructs 0 : Nat

succ n: Given a natural number n : Nat, constructs n + 1 : Nat.

Numerals such as 2 are syntax sugar for the corresponding iterated application of Nat<br>constructors. For example:

example : 0 = .zero := by rfl<br>example : 1 = .succ .zero := by rfl<br>example : 2 = .succ (.succ .zero) := by rfl

In these examples, we are stating a proposition that the two sides of the = sign are equivalent.<br>We prove the propositions using the rfl tactic that applies when the two sides<br>are identical by definition. We’ll go into more detail on tactics in the following sections.<br>The important take away for now is that instances of Nat are defined as the outputs of<br>iterated sequences of Nat constructors.

Functions

In this section...