2
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ 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? $\endgroup$ – nbro Aug 9 '20 at 10:48
2
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.