Writing a Theorem Prover from scratch

NOTE: I am no subject matter expert and have chose to learn about this field through utilizing LLMs to guide me using practical implementations. Also, I am assuming a basic familiarity with Haskell and the Functional Programming paradigm.

Our journey starts with the concept of lambda calculus and the existence of the Curry-Howard Correspondence. These concepts basically bridge the gap between Mathematics and Computer Science in a specific manner . This gives rise to a very interesting piece of software: theorem provers, which is a beautiful combination of compiler design, type theory and mathematics, three of my favourite concepts !

There aren’t many blogs on writing theorem provers from scratch, hence I thought I would fill the gap up myself! Now, to be fair, there is this excellent essay on writing one from scratch from Federico Carrone, who implements a very simple one in Python. Taking his implementation as the base starting point, I proceeded to re-implement, before moving on to a slightly more expressive one, which utilizes Dependant Type Theory.

I have extensively utilized LLMs to guide me (guide not code! Every line is hand-written by me) on creating the extended version, although at this stage, I do trust them to be excellent at this task (I must admit, it took some effort for me to get the LLMs to guide me in a manner that provided a smooth path to implement and understand the extended version). Without further ado, let’s jump in!

Version 1

The first version is essentially a copy of Federico’s version, as I wanted to start from a very basic and minimalist version. The only difference was that I re-wrote it in Haskell:

data Type
 = Atom String
 | Arrow Type Type
 deriving (Show, Eq)

data Term
 = Var String
 | Lam String Type Term
 | App Term Term
 deriving (Show, Eq)

type Context = [(String, Type)]

search :: Context -> String -> Type
search [] var = error ("unbound variable: " ++ var)
search ((k, v) : ctx) key
 | key == k = v
 | otherwise = search ctx key

extractright :: Type -> Type
extractright (Atom _) = error "Cannot be used on atoms"
extractright (Arrow _ r) = r

infer :: Term -> Context -> Type
infer term ctx = case term of
 Var var -> search ctx var
 Lam var t term -> let
 new_ctx = (var, t) : ctx
 body_type = infer term new_ctx
 in Arrow t body_type
 App fn arg -> let
 fn_type = infer fn ctx
 arg_type = infer arg ctx
 in extractright fn_type

The reason for choosing Haskell was that it was a natural fit for writing pure theorem provers, and provides exactly the kind of features which a high-level compiler/theorem prover needs. I would highly suggest reading Federico’s essay to properly grasp the V1 (it is an excellent essay!), and familiarity with it would be very useful for understanding concepts in this essay.

Before we move forward to the next step/version, I would like to demonstrate why we would need to extend it, and what we unlock by doing so. Let’s begin with the most trivial proof of all,

“Assuming , prove that exists.“

Or in other words, the Identity proof. If I had to write this statement in the above kernel, it would be:

// Here, it may seem like Atom "A" is some general type, it isn't. It's a specific term.
// Read the essay I mentioned to understand why!
Arrow (Atom "A") (Atom "A")

And our task is to provide a proof for this particular statement! The best analogy is to simply switch the terminology a bit: given this type, write me a function which adheres to it! In fact, for this case, we can effectively write this in good old Typescript as well:

type id = (input: string) : string

And the proof ? Well, we basically implement a function, which adheres to this type:

function id_proof (input: string) : string { return input }

// Note that the body of the function is itself treated as a proof, in the 
// mathematical sense! "Checking" a proof then simply means letting our compiler 
// make sure that the function body actually outputs the type we have mentioned 
// before

And in our kernel, we do the same: implement this function, and call the infer function on it

expr = Lam "x" (Atom "A") (Var "x")
infer expr 

// results in Arrow (Atom "A") (Atom "A"), or A -> A

Note how, in Typescript’s case, we had to specify a particular type. Basically, the statement itself is constrained to one particular type, the string, and is asking us to provide a proof for only that type. It’s the same case for our kernel as well, as the proof is only about a particular atom, “A“. It says nothing about another atom, say “B“.

This is a fundamental limitation about our system: in writing any statement and subsequently it’s proofs, we have to decide on the specifics, and hence cannot meaningfully provide proofs for more general statements, like:

“Assuming any , prove that exists.“

And this limitation leads us to our next version of the kernel, where we must rely on more advanced type systems.

Version 2: Why

Before we dive into the nitty-gritty details of how to implement a kernel that utilizes more advanced type theories, we must understand why we need it in the first place. As we saw at the end of the last section, if we stick to our old kernel, general statements/proofs remain out of our reach. In order to make these statements, I’d like to first point out what such a statement’s equivalent type must be … and the answer is : a function which takes in, as an input, a type! Or in other, more computer science terms, our kernel must be a system where Types are first-class citizens.

To be more precise, we must remember what a function (and it’s Type) represents in the first place. Referring to this table, again, from Federico’s blog:

The second to last row is basically what we are aiming for: a generic function. Can we do this in Typescript ?

type generic_id = (input : T) : T

And the corresponding proof/function definition simply becomes an implementation:

function generic_id_proof (input: T) : T { return input; }

The above implementation is basically a proof for the fact given any type, I have proven the Identity function. This level of type system is, in formal languages, also called System-F Polymorphism, which basically lets us write generics. At this point, most pragmatic use cases that are required by a programming language’s type system are satisfied, and hence, most languages tend not to go beyond this level.

But we have to go beyond ! When our goal is to write a theorem prover, we must set our eyes on more complex, more general proofs, which go beyond the capabilities of even system-F compilers. And for that, I will first extend our identity proof by another step:

“Assuming any , prove “

Here, two new terms have been introduced now: a Type family and an Indexed Type which we must clarify, before moving forward. To put it simply, a Family of Types is simply a function, which takes in any argument and returns a Type. In this case, we can view it as a function which takes in an object of a certain type, and outputs a Type rather than an object of another type, and this output is called the Indexed Type if this type depends on another, and the whole function is then called an Indexed Family of Types.

This all does seem very confusing, and we can really benefit from two things right now: understanding it through an example, and viewing it in action. First, I’d like to provide the necessary statement, and how it looks in lean4:

axiom id (A: Type U) (B: A -> Type V) (x: A) (input: B x) : B x

Here, Type U and Type V are some arbitrarily named types. And in the above example, B is our Indexed Type Family, and the output, B(x) is our Indexed type. This is essentially an example of Dependant Type Theory, where one type, the final output, is a dependant type, and it depends on the type of x we provide. Basically, whenever we have an output defined as an indexed type, which means it’s final type depends on another, we delve into DTT territory.

To drive this home, let’s look at an example. Imagine a particle moving through space. At some point in time, the particle has infinite ways it can move, at any speed. So let’s assign a type to it’s velocity: V. Now, let’s not assume a vacuum, which means this velocity at any point actually depends on it’s surroundings. Let’s call it the environment’s configuration , and assign it a type: Q. Which means the answer to the question of what’s the velocity of this particle, also begs the question of which configuration space are we talking about ? This means that, in order to get the final output, we must choose a particular configuration space, in which the said velocity exists. In the above syntax,

• First, we pick a certain velocity, x : V
• Next, we use it to pick a certain configuration space: Q(x), which translates to a particular configuration space, given this particular velocity.

This type system is basically essential if we have to deal with complex, abstract and generalized proofs in higher-level math, and Dependant Type Theory gives us the computational power to represent these types of proofs, in the form of programs.

Version 2 : Implementation

Now we finally arrive at the nitty-gritty details ! Lets first revisit what we are trying to achieve here: our types need to depend on others, just like how an output depends on an input. As I mentioned earlier, in formal systems, whenever we require an object to be an input it needs to be a first-class citizen, and it basically means that the system treats it as a primitive object. Most programming languages do not treat types as a primitive object. What that means is a function in that language cannot return a Type, it must always return a value and generally all types are erased at runtime . But we can’t have that, as one definition of a Type Family is that it’s basically a function that returns a type!

Whenever a primitive object depends on another, the latter must be a first class citizen within that language. For example, Int is the integer type, and let’s say the number, 1, is a value (of that type). What we want is for both to live at the same level of abstraction and more importantly, at the same level of computation. In general, types are just meta-data/values that live at compilation time, and are usually erased when the code actually runs (runtime). The problem is, at compile time the data (what I’ve been calling values) does not exist, and types do not exist during runtime. Letting one depend on the other gets really difficult

So now there are two ways we can do this, and in a surprising twist, these two ways give us the opposite end product! One gives us languages with minimal to no types at all, and the other gives us the highest-order implementations of the type system. Let us start with:

Why not persist types during runtime ?
Well, the whole point of compile time is to get the program ready to run, and by the time we reach runtime, we expect that program to have already followed the types we have specified, not to mention the memory overhead, costs and latency. BUT, we do do this, and we call it JIT or Just-In-Time compilation!

Although right now, we are more interested in doing the opposite: letting in values during compile time, which basically gives us Dependant Types, and we can now finally start with the very first step of the implementation: not treating types and data as different objects in the first place. We put both types and data under a unified umbrella, generally called Term in the literature, but I like the pragmatic name more, Expressions. So instead of our compiler treating types and values as separate objects, we let it treat them as one, and deal with the consequences. Here’s how we represent that in Haskell:

data Expr =
 Ref String
 | Level Int
 | FuncBn String Expr Expr
 | Lambda String Expr Expr
 | Apply Expr Expr
 deriving(Show, Eq)

Let’s go through what each term means in Expr:

• Ref String is basically any variable name, and “Ref“ is a short form for reference. So Ref “A“ means I am referring to the variable called “A“.
• Level Int is an intersting concept. Since we no longer distinguish between types and values, we have a conundrum. Think about it in this way, let suppose the number 1 has type Int, but Int itself must have a type! So we assign it one, let’s simply call it Type. Now I am sure you must’ve guessed the next step, what’s the type of Type ? In general, we simply assign it a type called Type 1, and it itself belongs to Type 2 and so on and so forth, and it’s basically what Level means here. It is the level in which our expression lives.
• FuncBn String Expr Expr is a short form for function binder. This is the Arrow type from the first kernel, but equipped to allow dependant types. A function binder basically allows it’s output expression (the last Expr) to mention the first expression (the middle Expr), using a bounded name (the first String), which it uses as a Ref. Here’s an example:
  FuncBn “x“ (Level 0) (Ref “x“) , in this expression, notice how the last expression can mention x, which was mentioned previously. While inferring this expression, we extend our known list of variables (temporarily) with the variable “x“, so that our last expression can “see“ it .
• Lambda String Expr Expr is basically just the actual application of the above function binders.
• Apply Expr Expr is also straightforward: we simply “apply“ the first expression on the second.

Now, given this primary object, we must write the relevant infer function, but more importantly, must implement these two features:

• α-equivalence
• β-reduction

While the names seem daunting, the concepts are shockingly simple.

α-equivalence asks us to implement an equal function, which returns true for expressions which are logically identical, and not just exactly equal. The difference is that if, between two expressions, the only difference they have is that of the names of their variables (the bounded variables), we treat them as equal.

// We have to write an "equal" function such that the below given expressions 
// are treated equal.

Lambda "x" (Level 0) (Ref "x")
Lambda "y" (Level 0) (Ref "y")

// But these two are not equal! Because their return variables are different, and their
// bound variables are never used. 

Lambda "x" (Level 0) (Ref "b")
Lambda "y" (Level 0) (Ref "c")

β-reduction is a function tasked with deciding what happens with a Lambda computes or basically, how are we supposed compute a function, given our function definition (the Lambda) and the input values. Here, we primarily rely on substitution to perform this computation . Here are a few examples of what I mean:

// We use it through the Apply expression.
// The below expression is basically applying our function, the lambda
// to an argument, the Ref "a"
Apply (Lambda "x" (Level 0) (Ref "x")) (Ref "a")

// The result of this would be:
Ref "a"
// Because, if we notice, the function returns whatever input it takes in
// as is. Although there's another condition that must be met, that the "a"
// must have a type of Level 0, to match the "x" in our Lambda.

With these functions out of our way, we have basically implemented our kernel! This version is equipped for using dependant types, and can satisfy the more general proofs of the kind I mentioned before. Finally, we must look at the inference rules for our system, through the infer function. Before we continue, I must mention that throughout inference, we must maintain a list of variables whose types we already know, either pre-specified by us or the ones that were inferred during a run and would need to be seen by the function later on. We call it the context, in Haskell: Bindings = [(String, Expr)] . Now, the inference rules are:

• In case of a Ref “a“ , we look through our context, and simple return what it points to. Error otherwise.
• In case of a Level N , we return Level N+1 , since, as I mentioned earlier, any Type living at level N, itself is of type N+1.
• In case of FuncBn “x“ (Level 0) (Ref “x“) , it resolved to a level, which tells us not only that this function definition is correct, but also the level it’s at. If our function can’t infer a level, we throw an error.
• In case of Lambda “x“ (Level 0) (Ref “x”), it resolves to a function binder. In this example: FuncBn “x“ (Level 0) (Ref “x”) .
• And in case of Apply (Lambda “x“ (Level 0) (Ref “x”)) (Ref "a") , we apply the beta-reduction rules in order to arrive at our final result, Ref “a“ in the above case.

With this, we have finally implemented our version 2 kernel! Looking back, most of the nuance came from simple AST (abstract syntax tree) manipulation, while trying to adhere to the correct semantics of the theory. For completion, here how we would represent and implement this proof:

// Proof statement: Assuming any , prove .
// In our kernel:

Lambda "A" (Level 0)
 (Lambda "B"
 (FuncBn "_" (Ref "A") (Level 0))
 (Lambda "x" (Ref "A")
 (Lambda "input"
 (Apply (Ref "B") (Ref "x"))
 (Ref "input"))))

// This may seem verbose, because it's in it's raw form
// In the above case, FuncBn starts with a "_" to represent a simpler, non-dependant
// function.

At this point, we can safely move on to the next steps, and implement more features to make this kernel more and more expressive, with the hopes of coming close to Lean’s core kernel, and explore other type theories!

Conclusion

One thing I learned by pulling back the curtain behind these seemingly complex theorem provers, which can represent the highest level of Mathematics is that it relies on some fundamental, very simple theories, which can be implemented through some very basic data structures (trees) and algorithms (tree manipulation). At least on this level.

Thank you for reading this far!

1. The correspondence is more about proofs and how they are equivalent to programs, rather than some general theory relating the two fields. We all know CS is derived from Math anyways.
2. A very trivial proof indeed. Although, there can be conditions/systems where we must first establish this before moving forward. Think temporal states, ownership conditions or, on a broader scale, environmental changes.
3. Notice how this proof is still very trivial, and is essentially still the Identity proof, just that the object in question has a complicated type, i.e, an indexed type.
4. As in, how the space around it is configured … Kindly keep in mind none of this is official/widely recognized terminology.
5. The one application that chatGPT gave me was it’s usage in General Relativity, which was really fascinating, I understood how we have used the language of DTT to express these beautiful and elegant concepts of differential geometry.
6. A lot of modern languages have some sort of workaround for this. Like Typescript’s type system being Turing Complete, Zig’s Comptime, Rust's dyn Trait or Associated Types or Haskell’s DataKinds extension.
7. In case anyone is wondering how can we have an output depend on multiple inputs, it’s through currying.
8. Beta-reduction is just a fancy way of saying function application.