Writing a Theorem Prover from scratch

NOTE: I am not a subject matter expert and have chosen to learn about this field by utilizing LLMs to guide me through 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 [1]. 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 myself! Now, to be fair, there is this excellent essay on writing one from scratch by Federico Carrone, who implements a very simple one in Python. Taking his implementation as the base starting point, I proceeded to re-implement it, before moving on to a slightly more expressive one, which utilizes Dependent 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!

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:

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 <Type>, prove that <Type> exists." [2]

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

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:

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

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".

"Assuming any <Type>, prove that <Type> exists."

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

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 its 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?

The above implementation is basically a proof for the fact that 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:

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 Lean 4:

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 Dependent Type Theory, where one type, the final output, is a dependent type, and it depends on the type of x we provide. Basically, whenever we have an output defined as an indexed type, which means its final type depends on another, we delve into DTT territory. [3]

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 its velocity: V. Now, let's not assume a vacuum, which means this velocity at any point actually depends on its surroundings. Let's call it the environment's configuration [4], 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,

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 Dependent Type Theory gives us the computational power to represent these types of proofs, in the form of programs. [5]

Now we finally arrive at the nitty-gritty details! Let's 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 [6]. 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 v