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.
Can we prove mathematical induction statements in Lisp?
functional programming;induction;proof assistants;lisp