Can we prove mathematical induction statements in Lisp?

Question

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.

Answer 1

Let me try to clarify a point that seems to be confusing you: you seem to be conflating 2 related, but different concepts.

• The first is the concept of a proof system, which allows you to specify and prove theorems about mathematics or computer science. Dependent types are one elegant way to do this, where the types are the specification language and the proofs are identified with programs, but this is not the only way to build a proof system! Isabelle allows you to specify and prove properties about programs, and is not based on dependent types or the Curry-Howard isomorphism/approach. The crucial takeaway is that these systems require the user to supply the proof.

• The second is the notion of automatic theorem proof systems (or provers) which take a specification language and automatically attempt to divine a proof. This means that ATP systems are in particular proof systems, where the user input for proofs is just a click on the "prove" button (actually most ATP systems allow and require a lot more input from the user). This state of affairs is of course quite desirable in theory, as it greatly relieves the burden for the user, and most proof systems integrate some capabilities of ATP.

With these clarifications in mind, my first answer is that Lisp is neither a proof system nor an ATP system. It is a programming language. As such, it cannot be said to prove anything as is. The Lisp language is untyped, so it doesn't even make sense to ask if its type system can be seen as a specification language.

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.

All this being said, there is a very notable ATP system that can specify and automatically prove things about (a small subset of) Lisp programs including your example: the ACL2 system. Hey, they even have your example in these slides! (They don't give the solution though).