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.

Improve this question
$\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
    Commented Aug 9, 2020 at 10:48

2 Answers 2

Reset to default
2
$\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.

Improve this answer
$\endgroup$
3
$\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.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .