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 fully verified HTTPS server, for example).
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
This follows on from my previous article which described how to get a simple Clojure Ring application running on AWS Lambda. This article shows how to connect it to a database.
The accompanying code is here.
AWS SAM provides direct support for DynamoDB, but not for more traditional databases like PostgreSQL, so that means dropping into CloudFormation. This is, sadly, rather wordy, because we'll need to configure all the neccessary AWS machinery (including setting up a VPC, security group, and database credentials) ourselves, but it's mostly standard boilerplate which is pretty well documented:
You can see the full CloudFormation template here. We'll explain the various sections in more detail below.
To avoid having to make our database publicly visible, we're going to put both our Lambda function and database in a shared VPC. Here's how we create that VPC:
VPC:
Type: AWS::EC2::VPC
Properties:
CidrBlock: 10.0.0.0/16
We also need to define a couple of subnets (RDS requires at least two subnets, in two different avaialability zones):
Subnet1:
Type: AWS::EC2::Subnet
Properties:
VpcId: !Ref VPC
CidrBlock: 10.0.1.0/24
AvailabilityZone: !Select [0, Fn::GetAZs: !Ref "AWS::Region"]
Subnet2:
Type: AWS::EC2::Subnet
Properties:
VpcId: !Ref VPC
CidrBlock: 10.0.2.0/24
AvailabilityZone: !Select [1, Fn::GetAZs: !Ref "AWS::Region"]
This is using a little CloudFormation magic to select the first two availability zones in whichever region we're deploying to. You could just as easily hardcode the availability zones if you prefer.
And we need a security group which allows things within the VPC to access Postgres:
SecurityGroup:
Type: AWS::EC2::SecurityGroup
Properties:
GroupDescription: !Sub "Security group for ${AWS::StackName}"
VpcId: !Ref VPC
SecurityGroupIngress:
- IpProtocol: tcp
FromPort: 5432
ToPort: 5432
CidrIp: !GetAtt VPC.CidrBlock
We put our Lambda function in the VPC we've created by adding the following to its Properties:
VpcConfig:
SecurityGroupIds: [!Ref SecurityGroup]
SubnetIds: [!Ref Subnet1, !Ref Subnet2]
Policies: [AWSLambdaVPCAccessExecutionRole]
We now have everything we need to create a database instance:
DBSubnetGroup:
Type: AWS::RDS::DBSubnetGroup
Properties:
DBSubnetGroupDescription: !Sub "DBSubnet group for ${AWS::StackName}"
SubnetIds: [!Ref Subnet1, !Ref Subnet2]
Database:
Type: AWS::RDS::DBInstance
Properties:
DBInstanceClass: db.t4g.micro
Engine: postgres
EngineVersion: 14.15
DBName: example_lambda_app
AllocatedStorage: 20
StorageEncrypted: true
ManageMasterUserPassword: true
MasterUsername: postgres
KmsKeyId: !Ref DatabaseKey
VPCSecurityGroups: [!Ref SecurityGroup]
DBSubnetGroupName: !Ref DBSubnetGroup
Most of this is pretty obvious: we're creating an RDS database running on a db.t4g.micro instance, with 20GB of storage, encrypted at rest, and with a master user called postgres. We're adding it to the security group we created earlier, and letting it know about the subnets we created via a DBSubnetGroup.
We've asked RDS to manage the database password for us (ManageMasterUserPassword) and store the credentials in a Secrets Manager (KMS) secret. Here's how we create that secret:
DatabaseKey:
Type: AWS::KMS::Key
Properties:
Description: DatabaseKey
EnableKeyRotation: false
KeyPolicy:
Version: 2012-10-17
Id: !Sub "key-${AWS::StackName}"
Statement:
- Effect: Allow
Principal:
AWS: !Sub "arn:${AWS::Partition}:iam::${AWS::AccountId}:root"
Action: ["kms:*"]
Resource: "*"
I've chosen to disable key rotation because I'll be passing the key to the Lambda function as an environment variable. An alternative would be to modify the Lambda function to use the Secrets Manager API to retrieve the password, but I wanted to keep the code as simple as possible. The rest is simple boilerplate taken from the article mentioned above.
To use this secret in our Lambda function, we add the following to the function's Properties:
Environment:
Variables:
DB_HOST: !GetAtt Database.Endpoint.Address
DB_PASSWORD: !Sub "{{resolve:secretsmanager:${Database.MasterUserSecret.SecretArn}:SecretString:password}}"
Deploying is exactly the same as before: build the uberjar and then sam deploy. The first time you do this it'll take a while because it's creating the database instance, but subsequent deployments will be much quicker.
Published: 2025-01-24
Tagged: clojure
I recently found myself starting a new project and was looking for the quickest and easiest way to get something up and running. In the past I might have used Heroku, and I looked briefly at Fly.io, but it turns out that Clojure now runs much better on Lambda than it used to (cold starts are no longer an issue), and it's easy to get up and running with AWS SAM which gives us simple serverless Infrastructure as Code.
This article describes how to get a simple Clojure Ring application running. A followup article shows how to connect it to a database. The code is available here.
Let's start with a simple Clojure Ring app with a sprinkling of interactivity through HTMX:
(ns example.lambda-app
(:require [compojure.core :refer [defroutes GET]]
[compojure.route :as route]
[hiccup2.core :refer [html]]
[ring.logger :refer [wrap-with-logger]]
[ring.middleware.defaults :refer [site-defaults wrap-defaults]]
[ring.middleware.params :refer [wrap-params]]))
(defn index-page
[]
(str (html [:head [:title "HTMX Example"]
[:script {:src "https://unpkg.com/htmx.org@2.0.4"}]]
[:body [:h1 "HTMX Example"]
[:div#greeting {:hx-get "/greet" :hx-trigger "load"}]])))
(defn greet [] (str (html [:div "Hello, World!"])))
(defroutes app-routes
(GET "/" [] (index-page))
(GET "/greet" [] (greet))
(route/not-found "Not Found"))
(def app
(-> app-routes
wrap-params
(wrap-defaults site-defaults)
wrap-with-logger))
This is all entirely standard: nothing different from any other Ring app. We're going to implement two different ways to serve this app, one using ring-jetty-adapter for local development, and one using ring-lambda-adapter for deployment to AWS Lambda.
For local development, we'll create dev/user.clj:
(ns user
(:require [ring.adapter.jetty :as jetty]
[example.lambda-app :refer [app]]))
(defn -main [& _]
(jetty/run-jetty #'app {:port 8080 :host "0.0.0.0" :join? false}))
And for deployment to AWS Lambda, we'll create lambda.clj:
(ns example.lambda
(:gen-class :implements
[com.amazonaws.services.lambda.runtime.RequestStreamHandler])
(:require [paulbutcher.ring-lambda-adapter :refer [handle-request]]
[example.lambda-app :refer [app]]))
(defn -handleRequest [_ is os _] (handle-request app is os))
This implements the RequestStreamHandler interface defined by the AWS Java Lambda runtime. The handle-request function is provided by ring-lambda-adapter and does the work of converting the input and output streams to and from Ring requests and responses.
Finally, here's our deps.edn:
{:paths ["src" "resources"]
:deps {com.amazonaws/aws-lambda-java-core {:mvn/version "1.2.3"}
com.amazonaws/aws-xray-recorder-sdk-slf4j {:mvn/version "2.18.2"}
com.paulbutcher/ring-lambda-adapter {:mvn/version "1.0.7"}
compojure/compojure {:mvn/version "1.7.1"}
hiccup/hiccup {:mvn/version "2.0.0-RC4"}
org.clojure/clojure {:mvn/version "1.12.0"}
ring-logger/ring-logger {:mvn/version "1.1.1"}
ring/ring-core {:mvn/version "1.13.0"}
ring/ring-defaults {:mvn/version "0.5.0"}}
:aliases {:run {:main-opts ["-m" "user"]}
:build {:deps {io.github.clojure/tools.build {:mvn/version "0.10.6"}}
:ns-default build}
:dev {:extra-paths ["dev"]
:extra-deps {org.slf4j/slf4j-simple {:mvn/version "2.0.16"}
ring/ring-jetty-adapter {:mvn/version "1.13.0"}}}}}
This is all very standard apart from:
aws-lambda-java-core which provides the AWS Java Lambda runtime.aws-xray-recorder-sdk-slf4j which turns SLF4J logs into AWS X-Ray traces.ring-lambda-adapter which provides a Ring adapter for AWS Lambda.You should now be able to run locally with clojure -M:dev:run.
To deploy to AWS, you'll need to have the AWS SAM CLI installed. This sits on top of AWS CloudFormation and simplifies the process of deploying serverless applications. Our application is described via a template.yaml file:
AWSTemplateFormatVersion: "2010-09-09"
Transform: AWS::Serverless-2016-10-31
Resources:
Function:
Type: AWS::Serverless::Function
Properties:
CodeUri: target/standalone.jar
Handler: example.lambda::handleRequest
Runtime: java21
FunctionUrlConfig:
AuthType: NONE
AutoPublishAlias: live
SnapStart:
ApplyOn: PublishedVersions
Timeout: 20
MemorySize: 512
Tracing: Active
Metadata:
SkipBuild: true
Outputs:
Endpoint:
Value: !GetAtt FunctionUrl.FunctionUrl
CodeUri points to an uberjar file we're going to build (the SkipBuild metadata tells SAM not to try to build the jar file itself).Handler is our Lambda function entry point.AuthType is NONE because this is a public web app (not an API that's sitting behind some kind of authentication).live), but we could have multiple aliases for different environments (e.g. staging etc.).SnapStart takes a snapshot of our function which reduces cold-start times to less than a second.Tracing enables AWS X-Ray tracing.To deploy, first build the jar file with clojure -T:build uber (see build.clj in GitHub), then deploy with sam deploy --guided. This will ask you some questions such as which region you want to deploy to and then eventually output the URL of your function's endpoint. Connect to that URL, and you should see exactly what you saw when you ran locally.
There are a number of different ways to keep an eye on how your Lambda function is performing.
sam logs --tail.[default.global.parameters] section to your samconfig.toml file.Local development works just like any other Ring app. To deploy a new version, just build a new jar file and run sam deploy.
The combination of SAM, which makes Lambda function deployment so simple, and SnapStart, which removes the cold start problem, means that AWS Lambda is my new default for getting started quickly.
In the next article, we'll look at how to connect our Lambda function to a database.
This was all heavily inspired by A Recipe for Plain Clojure Lambdas.
Published: 2025-01-23
Tagged: clojure