Niklas Gruhn / Blog
RSS feed LinkedIn GitHub logo

Lean explained with TypeScript

[TypeScript playground]

Lean is a programming language that lets you prove mathematical propositions. The Lean verifier automatically checks that these proofs are correct. This is the most formal and most bulletproof way to write proofs in mathematics. It's also incredibly tedious. Basic statements like a+b=b+a are not accepted without proof.

Lean has gained hugely in popularity with the advent of LLMs. LLMs write tons of code quickly but verification is laborious. Lean automates verification but the code is laborious to write. A match made in heaven!

This is not just useful for mathematicians. Lean is a general purpose programming language. For regular software it would also be nice to have more and stronger guarantees like:

What's mind blowing is that the Lean verifier is "just" a type checker. Propositions are expressed as types and proofs are written as values (aka terms). To prove a type/proposition is to write down a value of that type. The type checker simply checks (as usual): is this value/proof actually of that type/proposition. If yes, the proof is correct.

This might sound surprising. Usually it's not hard to find any value that matches a type. If anything, there are too many possible values and the sole reason we use types is to restrict the options.

Nevertheless, the Lean type system is not too different from a "normal one" like in TypeScript. Some fundamentals are strikingly similar. In fact, we can even prove simple propositions right in TypeScript. In the simplest form, it looks like this:

const proposition_name: PropositionAsType = proofAsValue

With the explicit type annotation, the type checker is forced to check whether proofAsValue is of type PropositionAsType. If yes, the proof is correct. Otherwise we get a type error. The problem with constants is we can't use type variables. We will need those. So we wrap all proofs with a dummy function:

function proposition_name<P,Q>(): PropositionAsType<P,Q> {
  return proofAsValue
}

Note: functions like this are not meant to be called. It's pure type trickery that becomes useless at runtime.

What are propositions?

Famous examples like Fermat's Last Theorem and the Riemann hypothesis come to mind. These are expressible in Lean but not in TypeScript. We have to start more basic: Any logical statement is a proposition. The most basic are true and false and any expression that "returns" a boolean can also be considered a proposition. So things built with &&, ||, ===, <=, isUpperCase(...), etc. But those are tools on the value-level. Propositions are written as types. We need all of that on the type-level.

Propositions as types

false

The proposition false is wrong! So it must not have a proof. In TypeScript, the corresponding type is never. Why? never is the empty type. By definition there is no value/proof you can return here:

function false_is_true(): never {
  return ???
}

Hence never/False has no proof. Well, TypeScript has escape hatches. Technically you can write:

function false_is_true(): never {
  return "obviously not never" as never
}

But that deliberately overrides the type system. It's like assuming 0=1. If you do that, all bets are off.

So never is the type-level version of false. To make it explicit, let's use a type alias from now on:

type False = never

true

true must have a proof. So there must be a value of that type. It doesn't really matter what that value is. We can define it as a type with a single dummy value:

type True = "dummy"

Here is the proof:

function true_is_true(): True {
  return "dummy"
}

AND / OR

Here is how to define boolean AND/OR on the type-level:

type And<P, Q> = { left: P, right: Q }
type Or<P, Q>  = { left: P } | { right: Q }

As a first example let's prove Or<True, False>. As you know true || false is true, so this proposition should have a proof:

function true_or_false(): Or<True, False> {
  return { left: "dummy" }
}

On the other hand true && false is false, so this can't have a proof. You can try but you get stuck:

function true_and_false(): And<True, False> {
  return { left: "dummy", right: ??? }
}

Go through the propositions below. Think about the analogous value-level expression. If it's true, it will have a proof. Try to write it down.

And<True, True>
And<False, True>
And<False, False>
Or<True, True>
Or<False, True>
Or<False, False>

PS: You can also write And using the intersection type operator (&). The resulting type is the same but now notice how similar the syntax is to value-level AND (p && q) and OR (p || q):

type And<P, Q> = { left: P } & { right: Q } // p && q
type Or<P, Q>  = { left: P } | { right: Q } // p || q

Implication

Implications (if P then Q) are everywhere. Not just in mathematical propositions:

In math/logic the standard symbol is =>. To use implications on the type-level, we can use arrow functions. The syntax matches again!

(p: P) => Q // if P then Q

Remember that every value is a proof. This implication gets a proof of P as argument and must return a proof of Q. To prove the implication itself is to show that such a function exists. Here is a simple example:

function P_implies_P_or_Q<P,Q>(): (p: P) => Or<P, Q> {
  return proofOfP => ({ left: proofOfP })
}

Here is something unintuitive. I think everyone will believe that false implies false. The proof works but wait a minute...

function false_implies_false(): (p: False) => False {
  return proofOfFalse => proofOfFalse
}

Didn't we say there is no value of type False? The proof receives a value of False as input and then returns it. Why is that even allowed? It's kinda like saying: If you give me a unicorn, I give you a unicorn back. Unicorns don't exist, so I know step 1 is never going to happen, but there is nothing wrong with step 1 implying step 2.

Here is the first proposition with a well known name:

type ModusPonens<P, Q> = (p_pq: And<P, (p: P) => Q>) => Q

In English: IF P is true AND P implies Q, then Q is also true. This was very confusing to me at first. Especially the nested implications. What does it even mean for an implication to imply something? But once you write down the proof and pick concrete types, it becomes completely obvious what's going on. This is just function application!

Instead of P/Q, think string/number. Then all this proposition is saying is: If you give me a string and something that turns a string into a number (length, word count, ...), then I can return a number.

Proof:

function modus_ponens<P, Q>(): ModusPonens<P, Q> {
  return ({ left: p, right: pq }) => pq(p)
}

Negation

Negation (written !p on value-level) is the least obvious one. You might expect some definition using conditional types:

// first try
type Not<P> = [P] extends [False] ? True : False

The problem is the condition can only be evaluated when P is a concrete type. That's not always the case. For example, try proving p implies !!p:

function P_implies_not_not_P<P>(): (p: P) => Not<Not<P>> {
  return p => ???
}

There is nothing you can write there. Not because the proposition is false but because the type checker doesn't even know what value to expect. It can't evaluate Not<Not<P>> to a concrete type.

We can make it work by defining Not differently. Using an implication:

type Not<P> = (p: P) => False

You may know that an implication p => q is equivalent to !p || q. If you replace q with false you get !p || false which is the same as !p. So it makes sense why you can define !p as p => false.

Now let's see the proof:

function P_implies_not_not_P<P>(): (p: P) => Not<Not<P>> {
  return p => not_p => not_p(p)
}

If you inline the Nots it's easier to see why it works:

(p: P) => (not_p: (p2: P) => False) => False

Equivalence

Equivalence is when both directions of an implication hold. So if both P implies Q and Q implies P:

type Equiv<P, Q> = And<(p: P) => Q, (q: Q) => P>

With that we can state and prove this famous law about booleans:

!(p || q) === (!p && !q)

This is the most verbose proof I'm going to show. I'm just going to leave it here. If you want to understand it, it's best you try and write it yourself. It's fun but it also gives you a glimpse how tedious Lean proofs can be.

function de_morgan<P, Q>(): Equiv<Not<Or<P, Q>>, And<Not<P>, Not<Q>>> {
  return {
    // !(p || q) => !p && !q
    left: not_p_or_q => ({ 
      left: p => not_p_or_q({ left: p }),
      right: q => not_p_or_q({ right: q }),
    }), 

    // !p && !q => !(p || q)
    right: not_p_and_not_q => p_or_q => {
      if ('left' in p_or_q) {
        return not_p_and_not_q.left(p_or_q.left)
      } else {
        return not_p_and_not_q.right(p_or_q.right)
      }
    },
  }
}

Conclusion

Learning to write proofs this way was very insightful to me. Writing traditional pen-and-paper proofs is a bit of an art. Obvious steps are often skipped, where "obvious" strongly depends on the author's judgement, implied knowledge, and the assumed audience. Writing proofs in Lean (or TypeScript) shows how incredibly mechanical the process can be.

The rabbit hole goes much deeper. But the core idea to take home is: