# Can a computer make a proof by induction?

Can a computer solve the following problem, i.e. make a proof by induction? And why?

Prove by induction that $$\sum_{k=1}^nk^3=\left(\frac{n(n+1)}{2}\right)^2, \, \, \, \forall n\in\mathbb N .$$

I'm doing a Ph.D. in pure maths. I love coding when I wanna have some fun, but I've never got too far in this field. I say my background because maybe there's someone who wants to explain this in a more abstract language there's a chance that I will understand it.

• Are you looking for any technique that is able to prove that statement, i.e. you are not necessarily looking for a machine learning approach, right? – nbro Aug 9 '20 at 10:48

There are programming languages that allow you to verify a proof by induction. For example, I used Coq, but I'm sure there are also others.

It is possible for some classes of problems. For instance, WolframAlpha can generate an induction proof to the problem posed in the question.

According to the author of this proof generator, he built a library of pattern-matched proofs to generate the proofs. More details about his approach can be find in his write-up about the problem.

Other alternative (thought not induction-based) for automatically verifying these kind of identities (in special, hypergeometric identities) is by using algorithms such as Zeilberger's method along with the HYPER algorithm, both described in the excellent book A=B, currently available for free by one of its co-authors.