Jul 11, 2018

3 comments

I.

When I sit down to write code, I can safely throw everything I can think of at the problem and just keep trying to run the code until it works—and when it works, I can actually see it working. If my code runs, it means I actually had to understand enough of the moving parts to get it to run. This is especially true in languages like Haskell with strong type constraints preventing me from doing anything too stupid.

When I sit down to prove a theorem, I have to be much more careful. One misstep in my reasoning and my whole proof will be invalid, without me even knowing I made a mistake until I or someone else catches it later. If my proof goes through, it's possible I understood enough of the moving parts to make it work, but it's also possible I didn't.

The standard solution to the problem of not having something to test your proof against when doing math is to use a proof checker, which lets you turn an arbitrary math problem into a programming problem. Instead of having to just get the right answer without ever being able to actually check your answer, you get lots of chances to test possible solutions.

Proof checkers are great, but traditional proof checkers are also pretty limited. Concepts like equality require specialized machinery like paramodulation to properly resolve, introducing new data types requires writing out long lists of PA-like axioms and in general modern functional programming tools that make writing out math easier like pattern-matching, ADTs, monads, etc. are just missing. When I wrote my own theorem prover/proof checker a while ago I ran into exactly these sorts of problems.

Dependent type theory is the modern way to solve all of these problems. Both equality and the natural numbers are defined just by giving the constructors, no axioms needed. For-alls and implications are just functions. Proving theorems really just feels like writing Haskell code.

I'm not going to try and give a dependent type theory tutorial here, because I don't think I would be able to do better than the one I used, Theorem Proving in Lean, which I highly recommend taking a look at. That being said, I do want to give a couple examples of what I mean before I move on. Don't worry if you don't understand this part, I just want to show you some actual code in a dependent type theory.

I said equality and the natural numbers were just data types, but to show you what I mean here is the actual definition of the natural numbers in the Lean standard library

`inductive nat`

| zero : nat

| succ (n : nat) : nat

where `:`

means "has type of." Those few lines are all that are required to completely define the semantics of the natural numbers—the induction rule is automatically synthesized from the above definition.

Equality is slightly more complex, but only because you need a little bit more boilerplate. Here is the actual definition of equality in the Lean standard library

`inductive eq {α : Sort u} (a : α) : α → Prop`

| refl : eq a

which is really just the Lean translation of the Haskell

`data Equals a = Refl`

where `eq a`

represents `a = a`

and `refl`

stands for reflexivity, the rule that `a = a`

always holds.

II.

Even despite all of the advances in automated proof checking with dependent type theory, there's still a big disadvantage to typing up all of your proofs in a dependent type theory like Lean: formality. When you write a proof by hand, you have the ability to elide over all sorts of details that you have to make explicit when you type them up into a proof checker. Thus, the main reason not to use a proof checker is the very reason to use one in the first place.

I think there exists a middle ground between these two extremes, however. One thing which has most impressed me working with Nate Soares is his ability to construct massive mathematical proofs on paper without a proof checker. When I asked him how he did this, he told me he used the type checker in his head. I've been trying to do this as well recently, and I want to try to share what that looks like.

Lawvere's theorem is a general result in category theory that states that if there exists a surjective function (technically but we'll elide that detail), then has the property that any function has some fixed point such that . To give you a sense of how important this theorem is, it's the general result underlying both Gödel's incompleteness theorems and Löb's theorem. I claim that Lawvere's theorem is nearly trivial to prove if you just imagine you have a type checker in your head.

Our starting environment, where the represents the thing we're trying to prove, is

from which point the only possible way to proceed is to use , which, under the interpretation where for-alls are functions, requires us to pass it some . If you think about how to construct a with the right type out of what we currently have available, there really aren't very many options. In fact, I think there are basically just the two: and , but since we know we're trying to prove something about , the definition with in it seems like the safest bet. Thus, we get

which, passing to