Can we prove mathematical induction statements in Lisp?
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).