Formal Verification With Lean

30 Apr 2026

Introduction

Lean is a functional programming language whose type system is powerful enough to encode mathematical proofs. One implication is that it is possible to use lean to write a program and to construct mathematical proofs about the its properties which are checked by the compiler. As an added benefit, lean comes with an interactive theorem prover which helps guide the process of converting mathematical statements into types.

The goal of this post is to introduce lean and walk through an example in which we implement insertion sort and prove that the output is always sorted.

We’ll