The Lean programming language is revolutionising mathematics. More and more mathematical results have been formalised in Lean and it's increasingly becoming a standard part of the mathematician's toolbox.
Lean didn't start out as a maths tool though; it was originally created to help with software verification: proving that software was correct.
This is not a new idea: software verification was all the rage when I was doing my PhD back in the early 1990s, but it never really took off. It was just too difficult and (outside of a few safety critical projects) nobody really used it in anger.
But, in just the same way that we recently crossed a threshold meaning that it's now realistic for mathematicians to automatically verify their proofs, that same threshold is rapidly approaching for software engineering. Combined with AI-assisted software engineering, it might already have been crossed.
In this article, I'm going to show you why I think that.
This is quite a long article, and the code behind it is also quite long. But (and this is the whole point) that doesn't matter because it's now cheap.
In just a few minutes with Claude Code, I got not just five different implementations of an algorithm, but I also got cast-iron proofs that they work as expected and are equivalent to each other (despite taking very different approaches). Not tests which suggest that they work, but a 100% guarantee.
Today, code isn't as important as it used to be. The real value is in the machinery around the code which allows you to confirm that it's correct. As Chad Fowler says in Evaluations Are the Real Codebase:
The durable asset is the thing that lets you regenerate with confidence: evaluations that encode what the system must do, independent of how any particular implementation does it.
Tests are one way to do that, but they're far from perfect. Lean allows us to create incontrovertable mathematically verified proofs that our code is correct, and AI assisted coding allows us to do so quickly and easily.
For this article, I'm going to use a little programming problem that I used to use when interviewing candidates. I wouldn't use it today, because AI agents have invalidated that approach to interviewing, but it's useful for our purposes because it's both simple enough to explain here, but also complicated enough to have a number of subtle pitfalls and edge cases. It can be solved in multiple different ways, each with their own tradeoffs. It's easy to state, but surprisingly difficult to get right.
We're going to create a function called partitionWhen which takes a list and a predicate (a function which takes an element of the list and returns either true or false). It partitions the list, returning a list of lists, where each sub-list starts whenever the predicate returns true.
Here's how we're going to test it:
#guard [1, 2, 0, 3, 4, 0, 5].partitionWhen (· == 0) == [[1, 2], [0, 3, 4], [0, 5]]
#guard ([] : List Nat).partitionWhen (· == 0) == []
#guard [0, 1, 2].partitionWhen (· == 0) == [[0, 1, 2]]
#guard [1, 2, 3].partitionWhen (· == 0) == [[1, 2, 3]]
#guard [0, 0, 0].partitionWhen (· == 0) == [[0], [0], [0]]
#guard is a Lean command which succeeds if the expression it's given is true and fails if it's false.#guard runs at compile time. So these tests will run (and succeed or fail) without having to be compiled and then run; just compiling is enough.(· == 0) is an anonymous function with the dot "·" showing where the argument should go. This is the same as x => x === 0 in JavaScript or lambda x: x == 0 in Python.Here's one way to implement partitionWhen in Lean:
def partitionWhen {α : Type _} (p : α → Bool) : List α → List (List α)
| [] => []
| [x] => [[x]]
| x :: y :: rest =>
match partitionWhen p (y :: rest) with
| g :: gs => if p y then [x] :: g :: gs else (x :: g) :: gs
| [] => [[x]]
α.p is our predicate function, which takes an α and returns a Bool.partitionWhen its predicate, what's left is a function which takes "a list of α (List α)" and returns "a list of lists of α (List (List α))".I encourage you to try implementing it in your own favourite language: it's slightly trickier than it initially seems. Here's the same approach implemented in a few other languages for comparison:
const partitionWhen = (p, xs) => {
if (xs.length === 0) return [];
if (xs.length === 1) return [[xs[0]]];
const [x, y, ...rest] = xs;
const result = partitionWhen(p, [y, ...rest]);
if (result.length === 0) return [[x]];
const [g, ...gs] = result;
return p(y) ? [[x], g, ...gs] : [[x, ...g], ...gs];
};
def partition_when(p, xs):
match xs:
case []:
return []
case [x]:
return [[x]]
case [x, y, *rest]:
match partition_when(p, [y, *rest]):
case []:
return [[x]]
case [g, *gs]:
return [[x], g, *gs] if p(y) else [[x, *g], *gs]
(defn partition-when [p xs]
(cond
(empty? xs) []
(empty? (rest xs)) [(list (first xs))]
:else
(let [[x y & more] xs
result (partition-when p (cons y more))]
(if (empty? result)
[(list x)]
(let [[g & gs] result]
(if (p y)
(cons (list x) (cons g gs))
(cons (cons x g) gs)))))))
defmodule PartitionWhen do
def partition_when(_p, []), do: []
def partition_when(_p, [x]), do: [[x]]
def partition_when(p, [x, y | rest]) do
case partition_when(p, [y | rest]) do
[g | gs] -> if p.(y), do: [[x], g | gs], else: [[x | g] | gs]
[] -> [[x]]
end
end
end
partitionWhen :: (a -> Bool) -> [a] -> [[a]]
partitionWhen _ [] = []
partitionWhen _ [x] = [[x]]
partitionWhen p (x : y : rest) =
case partitionWhen p (y : rest) of
[] -> [[x]]
(g : gs) -> if p y then [x] : g : gs else (x : g) : gs
let rec partitionWhen (p: 'a -> bool) : 'a list -> 'a list list =
function
| [] -> []
| [x] -> [[x]]
| x :: y :: rest ->
match partitionWhen p (y :: rest) with
| g :: gs -> if p y then [x] :: g :: gs else (x :: g) :: gs
| [] -> [[x]]
In just about any language other than Lean, we would now be done. We have our function, we have our tests, time to move on to the next problem.
Tests are great. The widespread adoption of automated testing is one of the best things to happen to Software Engineering over the last several decades.
But tests aren't perfect. However carefully we test, we're just checking a few examples and assuming that because our code works with them, it will work with whatever is thrown at it. How do we know that our tests have covered all the edge cases? Will partitionWhen work with any predicate? Will it works with lists of something other than natural numbers?
Sure, we can add more tests, but we have to stop somewhere. As the ISTQB says: "Testing shows the presence of defects, not their absence" and "Exhaustive testing is impossible".
partitionWhen correctHere's a theorem which, if we can find a way to prove it, will be true of any correct implementation of partitionWhen:
theorem partitionWhen_flatten {α : Type _} (p : α → Bool) :
∀ (xs : List α), (partitionWhen p xs).flatten = xs := by _
As in maths, the upside-down A "∀" means "for all". So this is saying "For any list xs of any type α, if we call partitionWhen on that list and then flatten the result, we should get our original list xs back".
Flatten takes a list of lists and turns it into a simple list by concatenating all sub-lists. So given [[1, 2], [0, 3, 4], [0, 5]] it will return [1, 2, 0, 3, 4, 0, 5]
So partitionWhen_flatten proves that no element is lost, duplicated, or reordered.
This isn't enough to guarantee that partitionWhen is correct on its own, but it is in combination with the following:
theorem partitionWhen_ne_nil_of_mem {α : Type _} (p : α → Bool) :
∀ (xs : List α), ∀ g ∈ partitionWhen p xs, g ≠ [] := by _
theorem partitionWhen_tail_false {α : Type _} (p : α → Bool) :
∀ (xs : List α), ∀ g ∈ partitionWhen p xs, ∀ z ∈ g.tail, p z = false := by _
theorem partitionWhen_head_true {α : Type _} (p : α → Bool) :
∀ (xs : List α), ∀ g ∈ (partitionWhen p xs).tail, ∀ z, g.head? = some z → p z = true := by _
In turn, these say:
It's worth taking a moment to convince yourself that these theorems, taken together, guarantee that partitionWhen is doing what we expect.
So how do we go about proving that these theorems are true?
There is a whole book on how Lean proves theorems and I'm not going to try to cover everything it says here. But it boils down to two things:
And that's it. Find an instance of the type and you're done.
Of course, that doesn't mean that finding that instance is easy 😜.
A couple of years ago, our only choice would have been to construct these proofs by hand. Lean's theorem prover is a great help, but it's still a laborious process for anything other than the simplest of proofs. So Lean would have been nothing more than an interesting footnote for most software engineers.
Today, however, AI agents are becoming very good indeed at generating proofs.
Here are complete proofs of all four of the theorems above. They run to around 160 lines of code, so I'm not going to reproduce them here. And as you can see they aren't the easiest to read or to follow. But:
In this, we're different from mathematicians. In most cases, a mathematician won't be happy with just knowing that something is true, they will also want to know why it's true. Ideally they don't just want a proof of whatever it is they're working on, they want a simple, elegant proof.
But in our case, we just want to know that the code we've written (or, more likely, that our AI agent has written on our behalf) is correct. An ugly proof that it's correct is just fine. The theorem is the important bit, the proof an implementation detail (think of it like you think of the machine code that comes out of your compiler).
Our implementation of partitionWhen doesn't just work, but it provably works, which puts it ahead of 99.999% of all code ever written (which is nice). But it's not perfect.
Like most functional langauges Lean supports tail recursion meaning that recursion won't blow up the stack. But this only works if calling itself is the last thing that a function does, which isn't true of partitionWhen.
No problem, it's not too difficult to create a tail recursive version:
def partitionWhenTR {α : Type _} (p : α → Bool) (xs : List α) : List (List α) :=
go xs [] []
where
go : List α → List α → List (List α) → List (List α)
| [], cur, acc => if cur.isEmpty then acc.reverse else (cur.reverse :: acc).reverse
| x :: xs, cur, acc =>
if p x && !cur.isEmpty then
go xs [x] (cur.reverse :: acc)
else
go xs (x :: cur) acc
Or, alternatively, we can make use of the foldl function provided by the Lean standard library (some languages call this reduce):
def partitionWhenFold {α : Type _} (p : α → Bool) (xs : List α) : List (List α) :=
let (groups, cur) := xs.foldl
(fun (acc : List (List α) × List α) x =>
let (groups, cur) := acc
if p x && !cur.isEmpty then
(cur.reverse :: groups, [x])
else
(groups, x :: cur))
([], [])
(if cur.isEmpty then groups else cur.reverse :: groups).reverse
There are another couple of implementations in the GitHub repository, one using takeWhile and dropWhile, and another using span.
I'm going to assert that all the above give exactly the same result as our first implementation, but it's not immediately obvious from looking at them.
In most languages, all we could do would be to test our new implementations and hope. In Lean, we could prove the same theorems as we proved for partitionWith. But we have another choice: we can prove that these new implementations are equivalent to our first implementation.
Here's an innocent looking little theorem:
theorem partitionWhenTR_eq_partitionWhen {α : Type _} (p : α → Bool) (xs : List α) :
partitionWhenTR p xs = partitionWhen p xs := _
It literally just says "partitionWhenTR is equal to partitionWhen". Easy to say, but how on Earth do you go about proving it? In general, it's not possible for an arbitrary program (this is very closely related to the famous Halting Problem), but it is possible for two programs that are guaranteed to terminate. And one of the nice things we haven't yet mentioned about Lean is that it is able to prove whether or not a function terminates (in fact every Lean function is guaranteed to terminate unless it's marked partial)
Here are proofs that all of the different implementations are equivalent. In this case, the proofs runs to over 500 lines of code, but again, these are 500 cheap lines, automatically generated by AI.
Which means that if we have some code which uses one of our partitionWhen implementations and we decide to swap to another, we can guarantee that its behaviour will be unchanged.
Lean is a full featured programming language capable of doing anything you can do in just about any other language. It's not as fast as some languages, but much faster than others (Python, we're looking at you).
What might stop you from using Lean in production is that all the focus has been on maths. Mathlib, the repository of reusable mathematical proofs is large and growing quickly; many of the things a working mathematician would expect to find are already there. The same is not true from the point of general software engineering. Reservoir, the repository of Lean packages, isn't especially well populated and a software engineer hoping to find a pre-built package which addresses their use case is likely to be disapointed. Although there are some gems in there (a formally verified regular expression engine and a zlib implementation, for example).
Also, as is obvious from this small example, each line of production code requires several lines of proof (perhaps a ratio of 1:10 or 1:20), which has cost implications (tokens at the very least).
But the benefit of knowing (not guessing, not hoping) that your code works is huge. With that in mind, I can only imagine that Lean will be of increasing importance to software engineers over time.
All the code in this article was created in VSCode configured as described here, Claude Code Pro, lean-lsp-mcp and Lean 4 Skills.
Published: 2026-07-08
Tagged: lean