HomeBlogNotesFood

home/blog/lean

Lean is pretty cool

2026.07.19


Lean is pretty cool. I think most people who know about Lean know it through the Mathlib Initiative and—considering that it’s properly named the Lean Theorem Prover and listed as “Lean (proof assistant)” on Wikipedia—hence think of it mostly in those terms as a purely academic project for the digitization of mathematics. And, to be fair, it is that. But it’s actually a very usable general-purpose programming language as well.

I’ve been intermittently using and exploring Haskell for a short while and I do love it for a number of reasons. I love that the syntax strikes a great balance between structured mathematical notation and practical text representation of a computer program1. I love its algebraic data types for all the reasons I love Rust enums plus the fact that I can write recursive types without having to manually add indirection to get around sizing considerations. And I even love that standard library’s most-used type classes like Functor, Semigroup, and Monad maintain a suitable degree of closeness to their mathematical foundations. But it also has some real annoyances. Overall, it looks like people mostly agree that a globally lazy execution model isn’t right for everything, and I think there’s a reason language extensions and compiler features like BangPatterns, StrictData, and -funbox-strict-fields exist: Laziness just doesn’t always pay off and most of the time people would prefer to have strict execution just because it’s easier to think about2. And while we’re at it, a few decades of very tight coupling to academic work has produced a compiler that’s overburdened with extensions and a language with too many idioms.

Here’s where Lean (properly, Lean 4) comes in. A short time ago I learned that, despite all of its abstract mathematical appeal, the Lean compiler actually compiles to C with reference-counted heap allocations and optimizations including safe mutation, producing native code that’s roughly on par with Haskell and OCaml, performance-wise. And on top of this, there are so many conveniences I wish were included in Haskell and OCaml, but with additional refinement for use in what I’m lightly thinking of as a kind of “post-monad” language (more on this below). But most importantly, Lean also makes use of its theorem-proving side for practical purposes in its ordinary functional programming side—you can totally use all the partial functions and handle all the error cases you want when doing ordinary programming, but if you take the time to prove concrete invariants in your program, you can actually use the proofs to make your code better!

So anyway, yeah, Lean is pretty cool. There are some downsides, as there must be, but for the moment I’m quite positive on it.

Introduction to Lean

Lean is a dependently typed, pure, functional, general-purpose programming language. Strictly, this post is talking about Lean 4, which was released in 2021 as the fourth implementation of the language (initially only experimental, of course) which was originally launched in 2013. Most notably, Lean has dependent typing3, and is based on something called the calculus of constructions. I don’t understand the calculus of constructions anywhere near well enough to talk about it in a post at this point, but Wikipedia says it’s a higher-order typed lambda calculus that apparently sits at a level of abstraction where it is both a typed programming language (clearly), as well as a constructive foundation for mathematics. In this respect, Lean is quite similar to Rocq, an “interactive theorem prover” with, as I understand it, near-identical goals. I haven’t done anything with Rocq, though, and—for whatever reason—the Mathlib project has chosen Lean instead, so I’ll only be talking about Lean here.

The Curry-Howard correspondence, as such

Lean’s major appeal is its ability to interact directly with the Curry-Howard correspondence. Here’s what I mean. Most languages in which you can write “proof-carrying code” typically force their proven propositions to be expressed via the structure of types—for instance, the proposition that a NonEmpty list is, in fact, non-empty (here in Haskell):

-- `NonEmpty a` can only be constructed by specifying at least one element
data NonEmpty a = a :| [a]

-- this function is total without using `Maybe` because each `NonEmpty` holds
-- its head element separate from all others
head :: NonEmpty a -> a
head (x0 :| _) = x0

Here, the structure of NonEmpty forces the non-empty proposition to be true. But nowhere in the code is it plainly stated, and the fact that it’s encoded in the structure of NonEmpty means that anytime we want a program to use the fact that a collection of data is non-empty it has to first convert to this particular form, which could carry runtime overhead.

In Lean, the Curry-Howard correspondence is given first-class treatment. Under the correspondence, a proposition is a type and evidence for the proposition is a value of that type. Hence, (evidence for) propositions can be passed around as ordinary values with a (possibly pretty complicated) proposition being written directly as its type. This means functions can explicitly list their assumptions in their signatures:

def head (items : Array a) (h : items.size > 0) : a :=
  items[0]

Here we have a function head that takes items, an ordinary Array—no special type structure—as well as evidence h that items is non-empty, and returns a (non-optional) value of item’s element type. Notice how we have a direct statement of what things head needs in order to work: nothing hides behind the definition of a struct or in the “Laws” part of a type class’s docstring.

In the body, the coll[idx] syntax calls into a method of a GetElem type class

class GetElem
    (coll : Type) (idx : Type) (elem : outParam Type)
    (valid : outParam (coll -> idx -> Prop)) where
  getElem (xs : coll) (i : idx) (h : valid xs i) : elem

which, for a collection type coll, and index type idx, requires an element type elem and a test valid that returns a condition that must be satisfied by a particular collection and index in order for the program using it to compile. For the standard library instance GetElem (Array a) Nat a, the test valid is essentially fun xs i => i < xs.size, and when Lean goes to compile head, a default proof tactic (more on this below) searches the scope of the function for things that imply it. Since head requires items.size > 0 (and we only use the 0 index), the body of head is then trivially an array access4. Notably, though, the fact that we have a proof that 0 is a valid index means the access is entirely safe!

One nice feature about treating proposition-types this way is that it adds incredible amounts of modularity and expressiveness when it comes to how these proven facts then get used by other parts of your code. Even if you can’t prove from first principles—essentially the structure of your program—that an array is non-empty, you can still mix runtime checks with type-propositions using what Lean calls a “dependent if”:

-- write to the head position and return the previous value if present
--
--                `×` is how Lean spells "tuple" --v
def setHead (val : a) (items : Array a) : Option a × Array a :=
  if nonempty : items.size > 0 then
    -- in this branch, `items.size` is indeed greater than 0;
    -- code here can use it as a proven fact under the name `nonempty`
    let oldHead := items[0]
    -- `Array.set` is another function that requires a proof of
    --   idx < array.size
    let newItems := Array.set items 0 val nonempty
    (some oldHead, newItems)
  else
    (none, items)

In this example, we’re using an ordinary runtime check of the size of items to prove items.size > 0, and calling the proof nonempty. This proof is used implicitly by the array access items[0], and then explicitly when we pass it to Array.set since we’d need to know that an index is in bounds before performing a write. And, by the way, having this proof actually does amount to real benefits. In this case, the compiler can use it to safely omit a bounds check in the emitted C (because we’ve done the check ourselves), and compile the non-empty branch to a raw pointer dereference/write!5

This is obviously a very simple example, but the ability to effectively pass around proofs as values provides a method to more easily ensure maintenance of program invariants between functions. Whereas in other languages proofs are heavily tied to the form of the relevant data, here they are free to be reasoned about in their own right, which lessens the need to convert between data representations whenever you want you add on conditions. If you still want to model a “parse, don’t validate” kind of flow to your program, the standard library provides Subtype, which is a simple association between a value and a proposition about it. Provided a proof to do so, the proposition can be freely changed independently of the value so that unnecessary runtime work regarding the representation of the data can be avoided:

-- roughly paraphrasing here...

-- a value that satisfies a predicate
structure Subtype a (p : a -> Prop) where
  -- the value
  val : a
  -- the proof of the predicate's truth
  property : p self.val

Let’s also consider a more complicated example. On several occasions in Haskell and Rust, I’ve wanted to construct a true enumerated type—that is, for a simple, finite, discrete type (ideally an enum or data with all unit variants/constructors), I want a one-to-one mapping to the natural numbers beginning at zero and ending at one less than the cardinality of the type6. Now, one might think this is relatively trivial to define. In Rust, unit variant-only enums are automatically coercible to usize using the as operator, and the Haskell standard library provides the Enum type class with methods toEnum :: Int -> a and fromEnum :: a -> Int. But these really aren’t strict enough: For instance, one can easily override the usize coercion in Rust or fromEnum in Haskell to map values to some non-contiguous subset of usize/Int, or have the map take two of the type’s values to the same integer, and that’s not even considering that the reverse mapping will almost certainly be a partial function with its own set of issues.

In Lean, we are given the tools to fully define such a thing properly:

-- witness to the cardinality of an enumerable type.
class Card (a : Type) where
  -- concrete bits
  card : Nat
  enum : Fin card -> a
  index : a -> Fin card
  -- proofs for the critical invariant
  enum_index : ∀ x, enum (index x) = x
  index_enum : ∀ i, index (enum i) = i

Here, Card proves that a given type a has cardinality card : Nat using a few nice proof-related structures. The first is Fin n, a subclass of Nat (the type of natural numbers) defined exactly as the combination of a number and a proof that the number is less than a finite upper bound:

structure Fin (n : Nat) where
  val : Nat
  isLt : val < n

Using Fin card, we identify the subset of natural numbers 0 ...< card as the exact codomain of our enumeration, defined as the combination of the class methods index and enum. Then to make the whole thing sound, we additionally require proofs enum_index and index_enum that the combination of index and enum give a true bijection between a and Fin card.

So then here’s an instance on an example data type:

inductive MyData where
  | a
  | b
  | c

instance : Card MyData where
  card := 3
  enum
    | 0 => .a
    | 1 => .b
    | 2 => .c
  index
    | .a => 0
    | .b => 1
    | .c => 2
  enum_index x := by cases x <;> rfl
  index_enum i := by decide

MyData is a simple sum type over unit constructors MyData.a, MyData.b, and MyData.c, with a cardinality clearly observable to be 3, which we then declare in the Card MyData instance immediately; enum and index then define the enumeration of MyData’s elements in the naive way7. We’ll talk more about proofs below, but Lean’s built-in proof tactics make for very succinct definitions of enum_index and index_enum. Essentially, enum_index says to, for x : MyData, split x into cases based on its available constructors. For each constructor case, substitute in the definitions of enum and index and check that the results satisfy the desired enum (index x) = x. Similarly, index_enum uses only a single tactic called decide, which uses the fact that Fin card has finite size to literally just go through all available inputs and check, again, that the desired index (enum i) = i holds.

To me, this is pretty incredible. I really can’t emphasize enough how great it is to describe program invariants in the exact terms of the procedure that would verify them, and of course to have them actually get checked by the compiler. There are several type classes and traits in Haskell and Rust that, for all the niceness that comes with a strong and expressive type system, ultimately fall a little short because they have no way of verifying that instances/implementors actually satisfy the various “laws” noted in their docstrings. The classic example is Hash, which always requires something to the effect of

(that is, values a and b hash to the same value if and only if they are actually the same value). In all fairness this is of course undecidable for infinite types like strings, but Rust and Haskell don’t have machinery to check for themselves whether it holds even for small/finite types. Not so in Lean, where we have the LawfulHashable type class:

class Hashable (a : Type) where
  hash : a -> UInt64

class LawfulHashable (a : Type) [BEq a] [Hashable a] where
  hash_eq (x : a) (y : a) : (a == b) = true -> hash a = hash b

Here we actually have the tools to express the invariant using the language we want to use it in, and a compiler that will verify it!

Haskell’s abstractions with OCaml’s conveniences

But the story doesn’t end there, because Lean as a language is shockingly expressive. What I’m about to talk about here is more syntax and ecosystem than semantics (which is to say mostly not inherent to the language), but I think it deserves a mention anyway. It has so many of the best aspects of my other favorite languages that I really can’t help but love it.

So clearly Lean already bears significant similarity to Haskell and OCaml, both of which I like. But I think it’s worth saying that it manages to derive the best features from both while inheriting none of either of their poorer design choices.

The namespacing problem

Here are some quick thoughts on OCaml. First, I love that OCaml mostly functions like a “get stuff done” version of Haskell. Like Haskell, there are nice abstract features like automatic currying, algebraic data types, and (mostly) unceremonious bounded polymorphism. But unlike Haskell, OCaml has strict execution, mutable data (sort of), and even loops. The module system, although significantly less flexible than type classes, is excellent at overcoming the common namespacing problem in a lot of functional languages. Let me give an example of this last one.

OCaml really encourages users to write their code in explicit modules through the module system itself. By grouping code within explicitly marked modules, it can be passed through module functors (not to be confused with the Haskell type class Functor), which are the main mechanism for ad-hoc polymorphism.

(* Abstract signatures for the usual `Functor` / `Monad` stack *)
module type Monad = sig
  (* The functor type *)
  type 'a m

  (* Pure/lift/return *)
  val return : 'a -> 'a m

  (* Apply a function through the functor *)
  val fmap : ('a -> 'b) -> 'a m -> 'b m

  (* Apply an effectful function *)
  val bind : ('a -> 'b m) -> 'a m -> 'b m
end

(* An OCaml "functor", giving derived monadic operations over lists *)
module MonadicOps (M : Monad) = struct
  (* Apply an action to each item; fold over the results from left to right *)
  let mapm (op : 'a -> 'b M.m) (items : 'a list) : ('b list) M.m =
    let work (acc : ('b list) M.m) (it : 'a) =
      M.bind (fun a -> op it |> M.mmap (fun x -> x :: a)) acc
    in List.fold_left work (M.return []) items |> M.mmap List.rev

  (* Fold an action over a list from left to right *)
  let foldm (op : 'b -> 'a -> 'b M.m) (init : 'b) (items : 'a list) : 'b M.m =
    let work (acc : 'b M.m) (it : 'a) : 'b M.m =
      M.bind (fun a -> op a it) acc
    in List.fold_left work (M.return init) items
end

Once interfaces are defined, they can be implemented on a concrete type (defined in its own module), and then the downstream operations that use the interfaces are explicitly derived.

module Maybe = struct
  (* The [Maybe] type for optional values *)
  type 'a t =
    | Nothing
    | Just of 'a

  let return = Just

  let fmap (f : 'a -> 'b) (mb : 'a t) : 'b t =
    match mb with
    | Nothing -> Nothing
    | Just x -> Just (f x)

  let bind (f : 'a -> 'b t) (mb : 'a t) : 'b t =
    match mb with
    | Nothing -> Nothing
    | Just x -> f x

  (* the input to a functor is allowed to provide a superset of functions *)
  let of_option (opt : 'a option) : 'a t =
    match opt with
    | None -> Nothing
    | Some x -> Just x
end

(* Now `mapm` and `foldm` are available on `Maybe.t` via `MaybeMonad.mapm` and
   `MaybeMonad.foldm` *)
module MaybeMonad = MonadicOps Maybe

This is a nice way of doing things. I typically prefer the Haskell way of doing it with type classes overall, but OCaml functors have the incredibly nice side effect of requiring that everything be confined to a concrete namespace. Whenever you want to run foldm with any particular monad, OCaml will require that the instantiation of foldm for that monad have already been declared somewhere in the program, such that one is never left guessing which foldm is actually being used.

On the other hand, though, this can lead to a verbosity problem if every use of a function not in an imported module requires full qualification. There’s an another feature in OCaml where you can effectively have expression-local imports of modules using Module.( ... ) syntax, for example:

(* obviously pretty contrived *)
let numbers =
  Seq.(
    (* all of these functions are sourced from the `Seq` namespace *)
    unfold (fun n -> if n < 100 then Some (n, 3 * n - 1) else None) 1
    |> mapi (fun k n -> n / (k + 1))
    |> take 3
  )

But this pretty clearly only really works as intended when you’re using at most a few different modules’ functions.

In Haskell, it’s even worse. We’re forced to import modules in one or more of three modes:

  1. Unqualified, bringing everything exported by the module into scope;
  2. unqualified with a provided list of target imports (no aliasing allowed);
  3. qualified, possibly with an alias.

It’s really no different from Rust or Python in principle, but there are two major differences from those languages. The first is that the name of the module from which a given function/type/type class is imported is in no way tied to the name of the package that provides it. This means third-party packages can (and typically do) define elements in the same module(s) as the standard library or other third-party packages, which makes it harder trace where an unfamiliar function comes from.

The second and more significant of the two is that in Haskell everything that’s not a type is either a function or a small collection of functions, including operators. So even though qualified imports can be used to avoid dumping all of a module’s contents into the global namespace, the trade-off is that it adds a ModuleName. prefix to essentially every independent operation you want to apply to your data. Where this becomes especially annoying is when a package has the gall to provide an operator that overlaps with one in Prelude, the standard library module, such as vector—which I should note is the ubiquitous contiguous-array library—replacing the append operator ++ or hmatrix replacing the semigroup multiplication operator <>. In these cases, you have to choose between explicitly agreeing to override Prelude with an extra import statement (it cannot be implicitly done because the compiler will later complain about not being able to choose by itself):

import Prelude hiding ((++), (<>))

or a qualified import, adding a prefix to each use of the operator:

import qualified Data.Vector as Vec
import qualified Numeric.LinearAlgebra as Mat

myVector :: Vec.Vector Int
myVector = a Vec.++ b
  where a = Vec.fromList [0, 1, 2]
        b = Vec.fromList [3, 4, 5]

myMatrix :: Mat.Matrix Double
myMatrix = a Mat.<> b
  where a = (3 Mat.>< 5) [1.0 .. 15.0]
        b = (5 Mat.>< 4) [1.0 .. 20.0]

(And don’t even get me started on trying to combine use of vector and hmatrix, which both export their own Vector type!)

The key thing here is that object-oriented languages, for all their faults, have a built-in mechanism for namespacing operations based on their operands. If your language has object classes, then the odds are pretty good that every operation you might ever need to perform on a object belonging to a given object class is defined as a method in that class or one of the other classes it interacts with. In these languages, this means you can get away with only importing the name of the class or a few relevant functions that construct objects belonging to the class.

Here’s where Lean comes in. In Lean, namespaces are a separate formal concept from package imports. Individual source files are imported (with no extra modes) to tell the compiler what source files need to be read, and namespaces are explicitly declared within those source files. Names can then be brought into scope in two ways: either through open, which supports constrained import lists (this time with per-item aliasing), or by simply entering the namespace, in which case subsequent definitions are also entered in the namespace.

/- File1.lean -/

namespace My.Space

inductive Expr where
  | lit : Float -> Expr
  | sym : String -> Expr
  | add : Expr -> Expr -> Expr
  | sub : Expr -> Expr -> Expr
  | mul : Expr -> Expr -> Expr
  | div : Expr -> Expr -> Expr

def eval : Expr -> Option Float
  | .lit x => some x
  | .sym _ => none
  | .add a b => eval a |>.join eval b |>.map (fun (a', b') => a' + b')
  | .sub a b => eval a |>.join eval b |>.map (fun (a', b') => a' - b')
  | .mul a b => eval a |>.join eval b |>.map (fun (a', b') => a' * b')
  | .div a b => eval a |>.join eval b |>.map (fun (a', b') => a' / b')

namespace Consts

def pi : Expr := .lit 3.141592653589793
def e : Expr := .lit 2.718281828459045

end Consts

end My.Space
/- File2.lean -/

-- if consuming from another file, we need an `import`
import Path.To.File1

-- all of `My.Space` is brought into scope
open My.Space

def exprA : Expr := .lit 3.14
def exprB : Expr := .sym "a"
example : eval (.add exprA exprB) = none := by native_decide
/- File3.lean -/

import Path.To.File1

-- or just work in the namespace
namespace My.Space

def exprC : Expr := .div Consts.pi Consts.e
example : eval exprC = some 5.859874482048838 := by native_decide

end My.Space

But here’s the really cool thing. If the type of a function’s operand matches the namespace it’s defined in, then it can be called using .method syntax, like in object-oriented languages8. So if, in the above, we had instead defined eval within My.Space.Expr, as in

namespace My.Space

inductive Expr where
  /- ... -/

namespace Expr

def eval (expr : Expr) : Option Float :=
  /- ... -/

end Expr
-- `def Expr.eval` would also have worked here

end My.Space

then we’d be able to write

-- import just the `Expr` type from `My.Space`
open My.Space (Expr)

def main : IO Unit := do
  let a := Expr.lit 1.0546e-34
  let b := Expr.sym "b"
  let expr := Expr.add a b
  let ans := expr.eval

If the function has more than one argument, then those arguments are substituted in after the . is applied:

def main : IO Unit := do
  let a : Array Nat := #[0, 1, 2, 3, 4]
  let b : Array String := #["hello", "goodbye"]
  IO.println <| toString <| a.zip b -- #[(0, hello), (1, goodbye)]

Single-argument functions can be strung together in the obvious way, e.g.

-- get the exponent for a scientific representation of a floating-point number
def Float.ord (val : Float) : USize :=
  if val == 0.0 then 0 else val.abs.log10.floor.toUSize

and multi-argument functions use a modified form of the pipe operator |>:

def clamp (xmin xmax x : Float) : Float :=
  x.min xmax |>.max xmin

It not only solves the namespace problem, it also nicely unifies struct field access with an application of a unary function. And, since third-party packages are free to declare things in any namespace they choose, it’s much easier for them to define custom behavior on single types without relying on an ad-hoc type class that’s meant only for one or a few specific types.

Purified mutability and loops

I think even if method syntax were the only major convenience, I’d still probably love it as much as I do now. But there’s another that I think is also worth calling out here. See, the main appeal of using a strongly typed, pure functional language is that everything is pure, and what would normally be impure, effectful code is made pure by tracking the effect somehow, usually in a monad. And, theoretically, this is all sound and guaranteed by well-studied math.

But the problem is that not everything is most easily expressed as a recursive function, or even a fold or traverse, for that matter. Sometimes, the most natural or readable expression of an algorithm still uses mutation and loops. It’s worth noting that OCaml recognizes this and almost begrudgingly still allows for imperative patterns with ref, for, and while. But this system is pretty rough, and it doesn’t look like there’s much work being put toward improving it—the clear indicator is that you’re forced to rely on exceptions and if to implement break and continue yourself:

exception Break

let () =
  let i = ref 0 in
  (try
    while true do
      if !i >= 10 then raise Break;
      Printf.printf "i = %d\n" !i;
      i := !i + 1
    done
  with Break -> ())

and I imagine it’s strongly related to the OCaml standard library’s weird, vestigial reliance on exceptions despite the language having existing option and result types.

Lean makes good on the theoretical promise of monads by making these imperative patterns available (including proper break and continue), but only within a monadic do.

def main : IO Unit := do
  let mut i := 0
  repeat do
    if i >= 10 then break
    IO.println s!"i = {i}"
    i := i + 1

And the great thing about this system is that it of course works with any monad. So if you need printing then you can use IO, but if all you need is mutation then the identity monad Id is also provided:

def squares (n : Nat) : Array Nat := Id.run do
  let mut nums : Array Nat := Array.emptyWithCapacity n
  for k in 0 ... n do
    nums := nums.push (k ^ 2)
  return nums

Whereas the addition of method syntax was vastly convenient, I think this is beautiful. Finally, a pure, functional language that actually uses monads to the fullest extent of what they’ve been claimed to do!

Modern standard library design

Of course, all of this speaks to a revised language design philosophy. One that has learned its lessons about purity and expressiveness, and arrived at something that can—ironically, given its pure mathematical appeal—capture the best of both imperative and functional programming. Here are a few examples.

First, there are no exceptions, only Option and Except9. I feel like this is a pretty standard thing to do nowadays, even in non-functional languages, but I just have to mention that OCaml’s standard library still has plenty of functions that raise exceptions instead of return its own result type. I don’t want to rag on it too hard because I’m sure there are legitimate historical reasons for this (considering their use in imperative patterns; see above), but it really is quite strange to me that OCaml—despite having all the tools to do so properly—has not made the standard library’s interfaces more consistent in their use of result10. (Yes, I’ve seen the third-party “alternative standard libraries” that attempt to rectify this, but my overall feelings on this are that you’re doing something wrong if users of your language feel like they need to make such a thing at all.)

The Lean standard library also wisely chooses to minimize the number of funky operators you need to know. Although the usual monad >>= and applicative functor <$>/*>/<*/<*> are still provided, it feels like they’re mostly used as a concession to the math/Haskell people: The standard library documentation makes it clear that >>= is merely syntactic sugar for the proper definition of the bind method of the standard Bind type class, and all standard monads provide bind as an ordinary function. (This is, of course, another upside to .method syntax. You can define your own operators, but there’s much less need to because x.bind f keeps all the operands in the same positions they’d be if you were to use >>=.)

In a similar vein, the prelude also splits up the standard Haskell Num class and provides the usual arithmetic operators as their own individual classes (like in Rust). In Haskell, the definition of Num assumes closure over a single type,

class Num a where
  (+) :: a -> a -> a
  (-) :: a -> a -> a
  (*) :: a -> a -> a
  {- ... -}

But of course this presents a problem because in mathematical contexts, these operations are often overloaded in deeply ingrained ways. For example, we can think of the different ways that matrices, vectors, and scalars all multiply in linear algebra. I think the Haskell people here would say that Num should only be instanced by proper numbers, but of course there are still pathologies you have to deal with, like what happens with Word (unsigned integers) under subtraction, that undermine the purity of the definition. I can respect the principled approach here, but the reality is that it’s simply a pain to have to use a custom operator for something as simple as addition11

In Lean, we have individual arithmetic classes

class HAdd a b (c : outParam Type) where
  hAdd : a -> b -> c

class HSub a b (c : outParam Type) where
  hSub : a -> b -> c

class HMul a b (c : outParam Type) where
  hMul : a -> b -> c

/- ... -/

where the “H” stands for “heterogeneous” (even though it could also stand for “homogeneous”). This is the right approach—there’s no monopolization of these basic operators, and it allows for more modular code overall since custom types are free to pick and choose which operations they implement rather than having +, -, and * always all required at once12.

Speaking of numbers, it’s nice to have unsigned integers in the standard library as well. Once again, Nat and the various UInt* types of the sort of thing you really expect to have in any language, but on the other hand there’s this discussion in a PR to add unsigned integers to the OCaml standard library that was eventually closed because of a weird obstinance toward them. It’s broadly related to purity and how to handle over/underflow, but some of the objections actually claim that they don’t have much utility—which is, of course, ridiculous (at minimum, think about what is being communicated when you see a UInt instead of an Int in a function signature!). And it’s not like Haskell is free from this either, considering that many prelude functions related to indexing use Int instead of Word, including the length of a list! Madness. To be honest, I have the vague impression from Lean that if natural numbers weren’t so important for termination proofs then its prelude wouldn’t have them either, but I’m glad they exist.

The final thing I want to mention is that the Lean prelude also provides native contiguous arrays. I don’t have much in particular to say about them—they still use boxed values, but are reference-counted and use in-place modification for unique instances—but it’s nice to not need a dependency on the Haskell vector package in every project.

Some math for spice

Now we can talk about proofs. Unfortunately, I mostly don’t have a vast patience for strict mathematical proofs—especially for things as mundane as index values being in-bounds—so I generally see the proof system as being broadly similar to how I think newcomers to Rust see the borrow checker. Which is to say that I understand its appeal and can appreciate all that it does for me… but it often gets in my way when I’m writing what should be something relatively straightforward13.

Partly this is due to what things end up requiring proofs as well as their phrasing, but in my opinion the proof system itself is also a little clunky. Let me explain how it works. Proofs, like functions (per Curry-Howard), are ultimately denoted as a series of steps by which a set of givens can be manipulated in order to imply a target. In the Lean proof system14, we work in the special type universe Prop, which is the set of all types that are directly logical propositions, like ∀ n : Nat, 0 ≤ n. In Prop, all terms of a fixed type are considered equal to each other—morally, we don’t care how a proposition is proven, only that it is—and so all the interesting operations are performed directly on the types of terms via rewrite operations known as tactics. The givens of a proof are generally called hypotheses in the compiler’s output terminology, and the target statement to be proven is known as the goal. Every proof is then a series of tactics that rewrite any of the hypotheses or the goal to directly show that the goal follows from the hypotheses, generally by satisfying any of a few criteria:

(Maybe I missed a couple, but probably these cover the vast majority of proofs that one will practically do.)

So let’s start off with a simple proof, say that ∀ n : Nat, 0 + n = n. As a standalone statement, this is written as a theorem:

theorem zero_add (n : Nat) : 0 + n = n :=
  /- proof body omitted -/

Here the syntax is deliberately similar to that for ordinary functions (again, per Curry-Howard). The “arguments” to the left of the colon are the initial set of hypotheses (here only that n is a Nat), and the conclusion to the right of the colon is the initial goal. Inside a proof, the compiler will keep a running table of what the hypotheses and goal are as different tactics are applied, which at the start of zero_add proof looks like this:

n : Nat     -- hypotheses go before the turnstile
⊢ 0 + n = n -- the goal comes after

Here’s an example body for zero_add:

theorem zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih => rw [Nat.add_one, Nat.add_succ, ih]

This is pretty terse (see Paper cuts), so let’s break it down. The proof starts off with the goal “state” as shown above, where we only know that n : Nat and want to prove 0 + n = n. In Lean, Nat is defined as an inductive type,

inductive Nat where
| zero : Nat
| succ : Nat -> Nat

and induction is a tactic that splits the proof into sub-goals based on the available constructors of some inductive (analogous to a match). Here, n : Nat, so we have two constructors and hence two sub-goals. The compiler knows that the zero case corresponds to the numeral 0, and gives us the sub-goal

⊢ 0 + 0 = 0

As I understand it, 0 + 0 is known to the compiler as being a decidable expression at compile time, and is evaluated to give 0 = 0. This is a tautology, and easily proven using the rfl tactic, which is short for “the reflexive property of equality”.

In the inductive case, succ, we’re tasked with proving that the truth of the conclusion for some k (the inductive hypothesis ih) also implies it for the successor k, denoted k.succ. The sub-goal in this case is

k : Nat
ih : 0 + k = k
⊢ 0 + (k + 1) = k + 1

and the following proof is just a bit more complicated. Here we have to make use of some helper theorems from the standard library, which are

theorem Nat.add_one (n : Nat) : n + 1 = n.succ

theorem Nat.add_succ (n m : Nat) : n + m.succ = (n + m).succ

rw [a, b, c, ...] is a tactic that takes a list of theorems and uses them in sequence as a rewrite rule on the goal: for each theorem of the form th : lhs = rhs, rw searches the goal for all instances of lhs and replaces it with rhs. In our proof, the results of these rewrites looks like this:

⊢ 0 + (k + 1) = k + 1   -- start
⊢ 0 + k.succ = k.succ   -- after rw [Nat.add_one]
⊢ (0 + k).succ = k.succ -- after rw [Nat.add_succ]
⊢ k.succ = k.succ       -- after rw [ih]

and the compiler closes the tautology automatically.

The body of the proof is then checked at compile time and erased—what exactly the proof was doesn’t matter as long as the check succeeds—and the theorem can later be applied to (in this case) Nats like a function or in other rw tactics. It’s also worth noting that other, high-level tactics like simp and tactic combinators like <;> exist to automate the rewriting and case-handling processes, but Lean’s proof system is, at its core, just about rewriting terms in Props.

And of course proofs can be extended to other kinds of propositions, like implications. For instance, we can prove that for any three Nats a, b, and c, we have that n + a = n + b implies a = b:

theorem add_left_cancel (a b n : Nat) : n + a = n + b -> a = b := by
  induction n with
  | zero =>
    intro h
    repeat rw [zero_add] at h
    exact h
  | succ k ih =>
    intro h
    repeat rw [Nat.add_one] at h
    repeat rw [Nat.succ_add] at h
    rw [Nat.succ_inj] at h
    exact ih h

There are a few additional tactics here. The first to be used is intro, which unpacks an implication lhs -> rhs in goal position by introducing or assuming lhs, and leaving rhs as the new goal. In the zero case, we start with the goal

| zero =>

-- a b : Nat
-- ⊢ 0 + a = 0 + b -> a = b

which becomes

  intro h

-- a b : Nat
-- h : 0 + a = 0 + b
-- ⊢ a = b

after intro h. We then use repeat to rw using zero_add specifically on h (instead of the goal) until zero_add can no longer be applied. After this we have

  repeat rw [zero_add] at h

-- a b : Nat
-- h : a = b
-- ⊢ a = b

and close the case by providing h as exactly the thing we are trying to prove.

The succ case unfolds similarly, with a starting goal

| succ k ih =>
  intro h

-- a b k : Nat
-- ih : k + a = k + b -> a = b
-- h : k + 1 + a = k + 1 + b
-- ⊢ a = b

after the intro. We then convert k + 1 to k.succ with Nat.add_one, and then collect terms inside the succs with Nat.succ_add (the left-addition version of add_succ from above) to get

  repeat rw [Nat.add_one] at h
  repeat rw [Nat.succ_add] at h

-- a b k : Nat
-- ih : k + a = k + b -> a = b
-- h : (k + a).succ = (k + b).succ
-- ⊢ a = b

Then we rewrite with a new theorem (the injectivity of the successor function)

theorem Nat.succ_inj (a b : Nat) : a.succ = b.succ <-> a = b
  rw [Nat.succ_inj] at h

-- a b k : Nat
-- ih : k + a = k + b -> a = b
-- h : k + a = k + b
-- ⊢ a = b

to remove the .succs, and then since implications are analogous to functions under Curry-Howard, we can apply ih to h to close the rest of the proof.

  exact ih h -- ih h : a = b

-- ⊢ True

So obviously proofs can get a lot more complicated (the entirety of Mathlib is a testament to that) but this is a little taste of what it’s like. If you’re interested in trying it out yourself and need something to prove, check out the Lean game server, which takes you through a curated list of some basic proofs in different areas of math. Beyond natural numbers, there’s some set theory, linear algebra, logic, and even real analysis (and more!).

Paper cuts

There are a few things I don’t like about Lean, however. Obviously none of these are bad enough for me to stop wanting to use it, but I think it’s only fair to mention them.

Proof interactivity and theorem discovery

The first and most major issue I have is that although the proof system works pretty well when you know what theorems are available, it’s often pretty hard to find what’s there when you don’t. What, for example, could a programmer do to complete the simple example proofs above if he didn’t know that Nat.add_one or Nat.succ_inj existed?

The answer is not much. Not very reliably, at least. The problem is that the collection of theorems provided in the standard library (not even including Mathlib) is huge. Even within the scope of just Nats, there are tons of individual theorems that all say only slightly different things about Nats. And of course it would be a Herculean task to add documentation describing even broadly when they could be useful, so combing through all of them just to find one or two that could be situationally useful for a handful of proofs in your program quickly turns into a slog.

There are other tools that can help a bit to guide the programmer here. For instance, you can write exact?/apply?/rw? in a proof to get the compiler to list existing theorems that it thinks may be relevant, but I find that it’s usually either like drinking from a fire hose in terms of how many things it returns (after all, it has to search through the space of essentially everything one could say about e.g. natural numbers) or just not that helpful. There’s also Loogle, which will allow you to search in the Hoogle style for particular theorem conclusions, e.g. ?a.succ = ?b.succ <-> ?a = ?b will, in fact, find Nat.succ_inj—but in sixth position out of a few dozen other mostly irrelevant theorems. And, of course, use of these tools presupposes that the programmer has some idea of what kinds of theorems could even be relevant to a proof. None of them will suggest which tactics to use, so if he also doesn’t really have a game plan going into the proof, then he’s really a bit screwed. (On this level, though, I’m willing to be a bit more forgiving because obviously proofs are an integral part of the language. Going into Lean without some familiarity with the available tactics is a bit like going into Python without know how to write classes.)

Additionally, a lot of the proof system design seems to assume that you’ll be using the proof checker in a strongly interactive fashion. That is, with a live readout of what the current goal state is and what hypotheses are in scope that updates as you add new lines to a proof. There are tools that generate this, of course—there’s lean.nvim, Lean 4 mode for Emacs, and a VS Code extension. This is all fine if you like this sort of thing, but I have a strong aversion to IDE-like elements in my editor—so I count this as a minor design flaw.

Special unicode characters

A bigger flaw (in my eyes), however, is the use of special unicode characters for many mathematical elements in the standard library and conventional notation. We have, (non-comprehensively):

Now, I should mention that none of these are strictly required: You don’t have to use ⟨...⟩ constructors, ←/↔/→ can always be replaced with <-/<->/->, there’s nothing stopping you from using the Latin alphabet for type variables, and technically all the logical and product/sum type symbols are “notation” for properly spelled-out parametric types like Prod, Exists, and Implies. And of course, you can set up your own input methods (e.g. Vim digraphs, X11 Compose) to make this less of a pain, but surely I can’t be alone in my annoyance here. What is it, really, that is to be gained by using × instead of * (as in OCaml), ∧ instead of the widely standardized &&? And, I get that in dependently typed languages you can no longer rely on parsing context to determine whether a variable a refers to a type or a term, but allowing Greek letters only encourages programmers to use single-character variables more (which, of course, everyone knows is a no-no).

Young/math-oriented ecosystem

It also must be said that Lean is a very new language with not only essentially no ecosystem, but a also a community that is obviously more focused on the proving/math side than the functional programming side. This mostly just is what it is; the proof checker is clearly the main innovation in the language. But currently the doc generator and REPL could both use some work, the compiler error messages are quite terse, and it would be nice to have other things like:

I realize that these are likely to be non-goals for a language with “Prover” in its name, but the language itself is just so nice that I can’t help but want to use it! I hope these eventually become goals for other people working in or on the language.

In the meantime, I’ve cobbled together some basic vibe-coded solutions for some of these:

Footnotes

  1. ↵ I also appreciate the purity of the various LISPs, but all those parentheses are seriously just plain silly.
  2. ↵ Separately, there’s also DuplicateRecordFields, NoFieldSelectors, NamedFieldPuns, OverloadedRecordDot, MutliParamTypeClasses, OverloadedStrings, and the entire existence of the Text type that, to me, indicate that several of Haskell’s design choices for Haskell were not made with the utmost foresight. This is forgivable, of course, but if the community is unwilling to start folding at least some of these extensions into the proper Haskell language, then at some point people just have to move on to a different language.
  3. ↵ Meaning that types can be described as functions of term-level values.

  4. ↵ A couple of additional technical points:

    • outParam Type is essentially a built-in marker used to assert to Lean that a type is knowable purely from the other non-outParam types in the local context, and can be thought of as the output of a Haskell type family or the consequent part of a functional dependency, or a Rust trait’s associated type.
    • Lean’s type system has a formal hierarchy of kinds of types—so it can reason about, for instance, “the type of all types that are instances of a given class”—Prop is the type of all types that are propositions. valid is a function that takes a particular collection of elements and an index into, and returns the proposition that must be satisfied for the index to be valid.
  5. ↵ It’s also worth noting that after a proposition is proven, the compiler is free to erase any concrete data associated with the proof and simply use the proposition on its own, which means all the proof stuff is zero-cost at runtime.
  6. ↵ In case anyone is wondering, this kind of thing comes up a lot if you’re doing physics-based linear algebra, where you have some sort of physical ordering to the rows or columns of a matrix.
  7. ↵ One syntactic convenience to note here is the existence of a standard library class OfNat, through which integer literals can be coerced to (in this case) Fin cards.
  8. ↵ I have no idea whether there’s anything causal here, but as I understand it, this is similar to Koka, where method syntax can be applied to any value whose type matches the first of a function’s arguments.
  9. ↵ This is perhaps confusing when comparing languages, but Except in Lean is just the equivalent of Result in Rust and Either in Haskell.
  10. ↵ For more weirdness, check out OCaml’s regex functions, which are even stateful: several functions implicitly refer to a match from the most recent call to a matching function in the control flow! Also, the fact that comparisons are done via integers, with compare a b returning any number less than 0 for less-than, 0 for equals, and any remaining number for greater-than. (Again, despite the language having everything it needs—i.e. simple sum types— to just have an ordering type instead!)
  11. ↵ See also OCaml, which skips the polymorphism entirely and makes you use separate operators for different numeric types, like +./-./*. for float (+/-/* are, of course, saved for integers).
  12. ↵ There may also be historical reasons why Num is in the Haskell prelude, considering that the equivalent definition of HAdd in Haskell would require extensions MultiParamTypeClasses and either FunctionalDependencies or TypeFamilies.
  13. ↵ I should also mention that—again, similar to Rust—the notion of what “should” be straightforward is one of those things that’s mostly based on experiences with other, more lenient languages. Just as the Rust compiler can make simple things complicated by enforcing a certain kind of strictness, the Lean compiler adds its own kind of strictness that happens to also induce this feeling. Whether one ultimately ends up learning to love or live with this kind of thing is, of course, up to the programmer.
  14. ↵ I have no idea how similar this is to Rocq’s system.

Changelog