# Can we prove mathematical induction statements in Lisp?

My previous question Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program? has a problem that it tries to cover too much ground. Here is a related question motivated by the comments.

In Lisp and certain other languages code and data are put on equal footing. Lisp is certainly strong enough to define abstractions, lazy evaluation and define types. I wonder if it is strong enough to prove simple statements about itself.

Important here... I only intend to prove specific theorems. It is quite clear we can't prove all theorems using any programming language.

Let's try: $1 + 2 + 3 + 4 + \dots + n = \frac{n(n+1)}{2}$. Then we statement:

$$P(1): 1 = \frac{1(1+1)}{2} \text{ and }P(n):1 + 2 + 3 + 4 + \dots + n = \tfrac{n(n+1)}{2}$$

We need to show that $\boxed{P(n) \to P(n+1)}$ this type of statement seems simple enough that we could try to verify it within Lisp itself. I could be wrong.

This couldn't be so hard. We have two functions:

• $F_1(n) = 1 + 2 + 3 + \dots + n$ and $F_2(n) = \frac{n(n+1)}{2}$

• In both cases there is some type of recursion $F(n+1) = (n+1) + F(n)$

• Then we could show the implication $F_1(n) = F_2(n) \to F_1(n+1) = F_2(n+1)$

The induction step should be expressible as a recursion. If the program itself can't prove induction statements, perhaps it can just summarize them in some kind of way.

In Haskell, the strong type means that once it compiles you have proven the types agree. This may not be as strong as proving other types of theorems.

I am not an expert in proof-checkers so excuse me if I get the basic concepts wrong.

My second answer is that Haskell is neither a proof system nor an ATP system. This seems to contradict the answer given to you here, but the point is that the Haskell type system closely reassembles a dependently typed proof system, to the extent that "specification-like" types can be given and "proof-like" programs can be written. One important limitation is that Haskell is not consistent when viewed as a logic. In particular, $1+1 = 3$ can easily be "proven" in a variety of different ways. Actual proof systems like Agda and Coq, however, can be used to specify and prove things about programs, which themselves can be extracted to Haskell programs.